{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PatternSynonyms #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

{-
 - Copyright (C) 2019-2020  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/>.
 -}

-- |

-- Module:        Data.Finitary

-- Description:   A type class witnessing that a type has finite cardinality.

-- Copyright:     (C) Koz Ross, 2019-2020

-- License:       GPL version 3.0 or later

-- Stability:     Experimental

-- Portability:   GHC only

--

-- This package provides the 'Finitary' type class, a range of useful

-- \'base\' instances for commonly-used finitary types, and some helper

-- functions for enumerating values of types with 'Finitary' instances.

--

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

-- > {-# LANGUAGE DerivingStrategies #-}

-- >

-- > import Data.Finitary (Finitary)

-- > import Data.Word (Word8, Word16)

-- > import GHC.Generics (Generic)

-- >

-- > data Foo = Bar | Baz (Word8, Word8) | Quux Word16

-- >    deriving stock (Eq, Generic)

-- >    deriving anyclass (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 indexes 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 (..),

    -- * Enumeration functions

    inhabitants,
    inhabitantsFrom,
    inhabitantsTo,
    inhabitantsFromTo,
  )
where

-- base

import Control.Applicative (Alternative (..), Const)
import Data.Bool (bool)
import Data.Functor.Identity (Identity)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Ord (Down (..))
import Data.Proxy (Proxy (..))
import Data.Semigroup (All, Any, Dual, First, Last, Max, Min, Product, Sum)
import Data.Void (Void)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Exts (proxy#)
import GHC.Generics
  ( (:*:) (..),
    (:+:) (..),
    Generic,
    K1 (..),
    M1 (..),
    Rep,
    U1 (..),
    V1,
    from,
    to,
  )
import GHC.TypeNats

-- finitary

import Data.Finitary.TH

-- finite-typelits

import Data.Finite
  ( finites
  , separateSum
  , shiftN
  , weakenN
  )
#if MIN_VERSION_finite_typelits(0,2,0)
import Data.Finite.Internal ( type Finite )
import Data.Finite.Internal.Integral ( pattern Finite )
#else
import Data.Finite.Internal ( Finite(..) )
#endif

#ifdef BITVEC
-- bitvec

import qualified Data.Bit as B
import qualified Data.Bit.ThreadSafe as BTS
#endif

#ifdef VECTOR
-- base

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

import Data.Finite
  ( combineProduct,
    separateProduct,
  )

-- typelits-witnesses

import GHC.TypeLits.Compare (isLE)

-- vector

import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Generic.Mutable as VGM

-- vector-sized

import qualified Data.Vector.Generic.Mutable.Sized as VGMS
import qualified Data.Vector.Generic.Sized as VGS
import qualified Data.Vector.Mutable.Sized as VMS
import qualified Data.Vector.Sized as VS
import qualified Data.Vector.Storable.Mutable.Sized as VSMS
import qualified Data.Vector.Storable.Sized as VSS
import qualified Data.Vector.Unboxed.Mutable.Sized as VUMS
import qualified Data.Vector.Unboxed.Sized as VUS
#endif

--------------------------------------------------------------------------------


-- | 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\'.

--

-- 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} \; (\texttt{Cardinality} \; a) \; \texttt{fromFinite} \; x = \texttt{fromFinite} \; y

-- \rightarrow x = y\]

--    * \[\forall x :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \exists y :: a \mid \texttt{fromFinite} \; x

-- = y\]

--

-- Furthermore, 'fromFinite' should be _order-preserving_. Namely, if @a@ is an

-- instance of @Ord@, we must have:

--

--    * \[\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} :: a = \texttt{fromFinite} \; \texttt{minBound} \]

--    * \[ a \neq \emptyset \rightarrow \texttt{end} :: a = \texttt{fromFinite} \; \texttt{maxBound} \]

--    * \[ \forall x :: a \; \texttt{end} :: a \neq x \rightarrow \texttt{next} \; x =

-- (\texttt{fromFinite} \circ + 1 \circ \texttt{toFinite}) \; x \]

--    * \[ \forall x :: a \; \texttt{start} :: a \neq x \rightarrow \texttt{previous} \; x =

-- (\texttt{fromFinite} \circ - 1 \circ \texttt{toFinite}) \; x \]

--

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

  -- | 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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a)
-> (Finite (GCardinality (Rep a)) -> Rep a Any)
-> Finite (GCardinality (Rep a))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (GCardinality (Rep a)) -> Rep a Any
forall x. Finite (GCardinality (Rep a)) -> Rep a x
forall (a :: Type -> Type) x.
GFinitary a =>
Finite (GCardinality a) -> a x
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 = Rep a Any -> Finite (GCardinality (Rep a))
forall x. Rep a x -> Finite (GCardinality (Rep a))
forall (a :: Type -> Type) x.
GFinitary a =>
a x -> Finite (GCardinality a)
gToFinite (Rep a Any -> Finite (GCardinality (Rep a)))
-> (a -> Rep a Any) -> a -> Finite (GCardinality (Rep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from

  -- | The first inhabitant, by index, assuming @a@ has any inhabitants.

  start :: (1 <= Cardinality a) => a
  start = Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite Finite (Cardinality a)
forall a. Bounded a => a
minBound

  -- | The last inhabitant, by index, assuming @a@ has any inhabitants.

  end :: (1 <= Cardinality a) => a
  end = Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite Finite (Cardinality a)
forall a. Bounded a => a
maxBound

  -- | @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 = (Finite (Cardinality a) -> a)
-> Maybe (Finite (Cardinality a)) -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality a) -> a)
-> (Finite (Cardinality a) -> Finite (Cardinality a))
-> Finite (Cardinality a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality a) -> Finite (Cardinality a)
forall a. Num a => a -> a
dec) (Maybe (Finite (Cardinality a)) -> Maybe a)
-> (a -> Maybe (Finite (Cardinality a))) -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite (Cardinality a) -> Bool)
-> Finite (Cardinality a) -> Maybe (Finite (Cardinality a))
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Finite (Cardinality a) -> Finite (Cardinality a) -> Bool
forall a. Eq a => a -> a -> Bool
/= Finite (Cardinality a)
forall a. Bounded a => a
minBound) (Finite (Cardinality a) -> Maybe (Finite (Cardinality a)))
-> (a -> Finite (Cardinality a))
-> a
-> Maybe (Finite (Cardinality a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
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 = (Finite (Cardinality a) -> a)
-> Maybe (Finite (Cardinality a)) -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality a) -> a)
-> (Finite (Cardinality a) -> Finite (Cardinality a))
-> Finite (Cardinality a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality a) -> Finite (Cardinality a)
forall a. Num a => a -> a
inc) (Maybe (Finite (Cardinality a)) -> Maybe a)
-> (a -> Maybe (Finite (Cardinality a))) -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite (Cardinality a) -> Bool)
-> Finite (Cardinality a) -> Maybe (Finite (Cardinality a))
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Finite (Cardinality a) -> Finite (Cardinality a) -> Bool
forall a. Eq a => a -> a -> Bool
/= Finite (Cardinality a)
forall a. Bounded a => a
maxBound) (Finite (Cardinality a) -> Maybe (Finite (Cardinality a)))
-> (a -> Finite (Cardinality a))
-> a
-> Maybe (Finite (Cardinality a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite

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 :: forall x. Finite (GCardinality V1) -> V1 x
gFromFinite = V1 x -> Finite 0 -> V1 x
forall a b. a -> b -> a
const V1 x
forall a. HasCallStack => a
undefined
  {-# INLINE gToFinite #-}
  gToFinite :: forall x. V1 x -> Finite (GCardinality V1)
gToFinite = Finite 0 -> V1 x -> Finite 0
forall a b. a -> b -> a
const Finite 0
forall a. HasCallStack => a
undefined

instance GFinitary U1 where
  type GCardinality U1 = 1
  {-# INLINE gFromFinite #-}
  gFromFinite :: forall x. Finite (GCardinality U1) -> U1 x
gFromFinite = U1 x -> Finite 1 -> U1 x
forall a b. a -> b -> a
const U1 x
forall k (p :: k). U1 p
U1
  {-# INLINE gToFinite #-}
  gToFinite :: forall x. U1 x -> Finite (GCardinality U1)
gToFinite = Finite 1 -> U1 x -> Finite 1
forall a b. a -> b -> a
const Finite 1
0

instance (Finitary a) => GFinitary (K1 _1 a) where
  type GCardinality (K1 _1 a) = Cardinality a
  {-# INLINE gFromFinite #-}
  gFromFinite :: forall x. Finite (GCardinality (K1 _1 a)) -> K1 _1 a x
gFromFinite = a -> K1 _1 a x
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 _1 a x)
-> (Finite (Cardinality a) -> a)
-> Finite (Cardinality a)
-> K1 _1 a x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite
  {-# INLINE gToFinite #-}
  gToFinite :: forall x. K1 _1 a x -> Finite (GCardinality (K1 _1 a))
gToFinite = a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite (a -> Finite (Cardinality a))
-> (K1 _1 a x -> a) -> K1 _1 a x -> Finite (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 _1 a x -> a
forall k i c (p :: k). K1 i c p -> c
unK1

instance (GFinitary a, GFinitary b) => GFinitary (a :+: b) where
  type GCardinality (a :+: b) = GCardinality a + GCardinality b
  {-# INLINE gFromFinite #-}
  gFromFinite :: forall x. Finite (GCardinality (a :+: b)) -> (:+:) a b x
gFromFinite = (Finite (GCardinality a) -> (:+:) a b x)
-> (Finite (GCardinality b) -> (:+:) a b x)
-> Either (Finite (GCardinality a)) (Finite (GCardinality b))
-> (:+:) a b x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (a x -> (:+:) a b x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (a x -> (:+:) a b x)
-> (Finite (GCardinality a) -> a x)
-> Finite (GCardinality a)
-> (:+:) a b x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (GCardinality a) -> a x
forall x. Finite (GCardinality a) -> a x
forall (a :: Type -> Type) x.
GFinitary a =>
Finite (GCardinality a) -> a x
gFromFinite) (b x -> (:+:) a b x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (b x -> (:+:) a b x)
-> (Finite (GCardinality b) -> b x)
-> Finite (GCardinality b)
-> (:+:) a b x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (GCardinality b) -> b x
forall x. Finite (GCardinality b) -> b x
forall (a :: Type -> Type) x.
GFinitary a =>
Finite (GCardinality a) -> a x
gFromFinite) (Either (Finite (GCardinality a)) (Finite (GCardinality b))
 -> (:+:) a b x)
-> (Finite (GCardinality a + GCardinality b)
    -> Either (Finite (GCardinality a)) (Finite (GCardinality b)))
-> Finite (GCardinality a + GCardinality b)
-> (:+:) a b x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (GCardinality a + GCardinality b)
-> Either (Finite (GCardinality a)) (Finite (GCardinality b))
forall (n :: Nat) (m :: Nat).
KnownNat n =>
Finite (n + m) -> Either (Finite n) (Finite m)
separateSum
  {-# INLINABLE gToFinite #-}
  gToFinite :: forall x. (:+:) a b x -> Finite (GCardinality (a :+: b))
gToFinite (L1 a x
x) = Finite (GCardinality a) -> Finite (GCardinality a + GCardinality b)
Finite (GCardinality a) -> Finite (GCardinality (a :+: b))
forall (n :: Nat) (m :: Nat). (n <= m) => Finite n -> Finite m
weakenN (Finite (GCardinality a) -> Finite (GCardinality (a :+: b)))
-> (a x -> Finite (GCardinality a))
-> a x
-> Finite (GCardinality (a :+: b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a x -> Finite (GCardinality a)
forall x. a x -> Finite (GCardinality a)
forall (a :: Type -> Type) x.
GFinitary a =>
a x -> Finite (GCardinality a)
gToFinite (a x -> Finite (GCardinality (a :+: b)))
-> a x -> Finite (GCardinality (a :+: b))
forall a b. (a -> b) -> a -> b
$ a x
x
  gToFinite (R1 b x
x) = Finite (GCardinality b) -> Finite (GCardinality a + GCardinality b)
Finite (GCardinality b) -> Finite (GCardinality (a :+: b))
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m, n <= m) =>
Finite n -> Finite m
shiftN (Finite (GCardinality b) -> Finite (GCardinality (a :+: b)))
-> (b x -> Finite (GCardinality b))
-> b x
-> Finite (GCardinality (a :+: b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b x -> Finite (GCardinality b)
forall x. b x -> Finite (GCardinality b)
forall (a :: Type -> Type) x.
GFinitary a =>
a x -> Finite (GCardinality a)
gToFinite (b x -> Finite (GCardinality (a :+: b)))
-> b x -> Finite (GCardinality (a :+: b))
forall a b. (a -> b) -> a -> b
$ b x
x

instance (GFinitary a, GFinitary b) => GFinitary (a :*: b) where
  type GCardinality (a :*: b) = GCardinality a * GCardinality b
  {-# INLINABLE gFromFinite #-}
  gFromFinite :: forall x. Finite (GCardinality (a :*: b)) -> (:*:) a b x
gFromFinite Finite (GCardinality (a :*: b))
i =
    let (Finite (GCardinality a)
x, Finite (GCardinality b)
y) = Finite (GCardinality a * GCardinality b)
-> (Finite (GCardinality a), Finite (GCardinality b))
forall (n :: Nat) (m :: Nat).
KnownNat m =>
Finite (n * m) -> (Finite n, Finite m)
separateProduct' Finite (GCardinality a * GCardinality b)
Finite (GCardinality (a :*: b))
i
     in Finite (GCardinality a) -> a x
forall x. Finite (GCardinality a) -> a x
forall (a :: Type -> Type) x.
GFinitary a =>
Finite (GCardinality a) -> a x
gFromFinite Finite (GCardinality a)
x a x -> b x -> (:*:) a b x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Finite (GCardinality b) -> b x
forall x. Finite (GCardinality b) -> b x
forall (a :: Type -> Type) x.
GFinitary a =>
Finite (GCardinality a) -> a x
gFromFinite Finite (GCardinality b)
y
  {-# INLINABLE gToFinite #-}
  gToFinite :: forall x. (:*:) a b x -> Finite (GCardinality (a :*: b))
gToFinite (a x
x :*: b x
y) = forall (n :: Nat) (m :: Nat).
KnownNat m =>
(Finite n, Finite m) -> Finite (n * m)
combineProduct' @(GCardinality a) @(GCardinality b) (Finite (GCardinality a) -> Finite (GCardinality a)
forall (n :: Nat) (m :: Nat). (n <= m) => Finite n -> Finite m
weakenN (Finite (GCardinality a) -> Finite (GCardinality a))
-> (a x -> Finite (GCardinality a))
-> a x
-> Finite (GCardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a x -> Finite (GCardinality a)
forall x. a x -> Finite (GCardinality a)
forall (a :: Type -> Type) x.
GFinitary a =>
a x -> Finite (GCardinality a)
gToFinite (a x -> Finite (GCardinality a)) -> a x -> Finite (GCardinality a)
forall a b. (a -> b) -> a -> b
$ a x
x, Finite (GCardinality b) -> Finite (GCardinality b)
forall (n :: Nat) (m :: Nat). (n <= m) => Finite n -> Finite m
weakenN (Finite (GCardinality b) -> Finite (GCardinality b))
-> (b x -> Finite (GCardinality b))
-> b x
-> Finite (GCardinality b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b x -> Finite (GCardinality b)
forall x. b x -> Finite (GCardinality b)
forall (a :: Type -> Type) x.
GFinitary a =>
a x -> Finite (GCardinality a)
gToFinite (b x -> Finite (GCardinality b)) -> b x -> Finite (GCardinality b)
forall a b. (a -> b) -> a -> b
$ b x
y)

instance (GFinitary a) => GFinitary (M1 _x _y a) where
  type GCardinality (M1 _x _y a) = GCardinality a
  {-# INLINE gFromFinite #-}
  gFromFinite :: forall x. Finite (GCardinality (M1 _x _y a)) -> M1 _x _y a x
gFromFinite = a x -> M1 _x _y a x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (a x -> M1 _x _y a x)
-> (Finite (GCardinality a) -> a x)
-> Finite (GCardinality a)
-> M1 _x _y a x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (GCardinality a) -> a x
forall x. Finite (GCardinality a) -> a x
forall (a :: Type -> Type) x.
GFinitary a =>
Finite (GCardinality a) -> a x
gFromFinite
  {-# INLINE gToFinite #-}
  gToFinite :: forall x. M1 _x _y a x -> Finite (GCardinality (M1 _x _y a))
gToFinite = a x -> Finite (GCardinality a)
forall x. a x -> Finite (GCardinality a)
forall (a :: Type -> Type) x.
GFinitary a =>
a x -> Finite (GCardinality a)
gToFinite (a x -> Finite (GCardinality a))
-> (M1 _x _y a x -> a x) -> M1 _x _y a x -> Finite (GCardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 _x _y a x -> a x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1

-- * Instances

-- Basic types


instance Finitary Void

instance Finitary ()

instance Finitary (Proxy a)

instance Finitary Bool

instance Finitary Any

instance Finitary All

#ifdef BITVEC
instance Finitary B.Bit where
  type Cardinality B.Bit = 2
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Bit) -> Bit
fromFinite = Bool -> Bit
B.Bit (Bool -> Bit) -> (Finite 2 -> Bool) -> Finite 2 -> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool
forall a. Enum a => Int -> a
toEnum (Int -> Bool) -> (Finite 2 -> Int) -> Finite 2 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite 2 -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE toFinite #-}
  toFinite :: Bit -> Finite (Cardinality Bit)
toFinite = Int -> Finite 2
forall a. Enum a => Int -> a
toEnum (Int -> Finite 2) -> (Bit -> Int) -> Bit -> Finite 2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Int
forall a. Enum a => a -> Int
fromEnum (Bool -> Int) -> (Bit -> Bool) -> Bit -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bit -> Bool
B.unBit
  {-# INLINE start #-}
  start :: (1 <= Cardinality Bit) => Bit
start = Bit
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Bit) => Bit
end = Bit
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Bit -> Maybe Bit
next = (Bit -> Bit) -> Maybe Bit -> Maybe Bit
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Bit -> Bit
forall a. Enum a => a -> a
succ (Maybe Bit -> Maybe Bit) -> (Bit -> Maybe Bit) -> Bit -> Maybe Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Bool) -> Bit -> Maybe Bit
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
forall a. Bounded a => a
minBound)
  {-# INLINE previous #-}
  previous :: Bit -> Maybe Bit
previous = (Bit -> Bit) -> Maybe Bit -> Maybe Bit
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Bit -> Bit
forall a. Enum a => a -> a
pred (Maybe Bit -> Maybe Bit) -> (Bit -> Maybe Bit) -> Bit -> Maybe Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Bool) -> Bit -> Maybe Bit
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
forall a. Bounded a => a
maxBound)

instance Finitary BTS.Bit where
  type Cardinality BTS.Bit = 2
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Bit) -> Bit
fromFinite = Bool -> Bit
BTS.Bit (Bool -> Bit) -> (Finite 2 -> Bool) -> Finite 2 -> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool
forall a. Enum a => Int -> a
toEnum (Int -> Bool) -> (Finite 2 -> Int) -> Finite 2 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite 2 -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE toFinite #-}
  toFinite :: Bit -> Finite (Cardinality Bit)
toFinite = Int -> Finite 2
forall a. Enum a => Int -> a
toEnum (Int -> Finite 2) -> (Bit -> Int) -> Bit -> Finite 2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Int
forall a. Enum a => a -> Int
fromEnum (Bool -> Int) -> (Bit -> Bool) -> Bit -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bit -> Bool
BTS.unBit
  {-# INLINE start #-}
  start :: (1 <= Cardinality Bit) => Bit
start = Bit
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Bit) => Bit
end = Bit
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Bit -> Maybe Bit
next = (Bit -> Bit) -> Maybe Bit -> Maybe Bit
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Bit -> Bit
forall a. Enum a => a -> a
succ (Maybe Bit -> Maybe Bit) -> (Bit -> Maybe Bit) -> Bit -> Maybe Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Bool) -> Bit -> Maybe Bit
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
forall a. Bounded a => a
minBound)
  {-# INLINE previous #-}
  previous :: Bit -> Maybe Bit
previous = (Bit -> Bit) -> Maybe Bit -> Maybe Bit
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Bit -> Bit
forall a. Enum a => a -> a
pred (Maybe Bit -> Maybe Bit) -> (Bit -> Maybe Bit) -> Bit -> Maybe Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Bool) -> Bit -> Maybe Bit
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Bit -> Bit -> Bool
forall a. Eq a => a -> a -> Bool
== Bit
forall a. Bounded a => a
maxBound)
#endif

instance Finitary Ordering

-- | 'Char' has one inhabitant per Unicode code point.

instance Finitary Char where
  type Cardinality Char = $(charCardinality)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Char) -> Char
fromFinite = Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> (Finite 1114112 -> Int) -> Finite 1114112 -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite 1114112 -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE toFinite #-}
  toFinite :: Char -> Finite (Cardinality Char)
toFinite = Int -> Finite 1114112
forall a. Enum a => Int -> a
toEnum (Int -> Finite 1114112) -> (Char -> Int) -> Char -> Finite 1114112
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE start #-}
  start :: (1 <= Cardinality Char) => Char
start = Char
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Char) => Char
end = Char
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Char -> Maybe Char
next = (Char -> Char) -> Maybe Char -> Maybe Char
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Char
forall a. Enum a => a -> a
succ (Maybe Char -> Maybe Char)
-> (Char -> Maybe Char) -> Char -> Maybe Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> Char -> Maybe Char
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Char -> Maybe Char
previous = (Char -> Char) -> Maybe Char -> Maybe Char
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Char
forall a. Enum a => a -> a
pred (Maybe Char -> Maybe Char)
-> (Char -> Maybe Char) -> Char -> Maybe Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> Char -> Maybe Char
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
forall a. Bounded a => a
minBound)

instance Finitary Word8 where
  type Cardinality Word8 = $(cardinalityOf @Word8)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Word8) -> Word8
fromFinite = Int -> Word8
forall a. Enum a => Int -> a
toEnum (Int -> Word8) -> (Finite 256 -> Int) -> Finite 256 -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite 256 -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE toFinite #-}
  toFinite :: Word8 -> Finite (Cardinality Word8)
toFinite = Int -> Finite 256
forall a. Enum a => Int -> a
toEnum (Int -> Finite 256) -> (Word8 -> Int) -> Word8 -> Finite 256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE start #-}
  start :: (1 <= Cardinality Word8) => Word8
start = Word8
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Word8) => Word8
end = Word8
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word8 -> Maybe Word8
next = (Word8 -> Word8) -> Maybe Word8 -> Maybe Word8
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word8 -> Word8
forall a. Enum a => a -> a
succ (Maybe Word8 -> Maybe Word8)
-> (Word8 -> Maybe Word8) -> Word8 -> Maybe Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word8 -> Bool) -> Word8 -> Maybe Word8
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word8
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Word8 -> Maybe Word8
previous = (Word8 -> Word8) -> Maybe Word8 -> Maybe Word8
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word8 -> Word8
forall a. Enum a => a -> a
pred (Maybe Word8 -> Maybe Word8)
-> (Word8 -> Maybe Word8) -> Word8 -> Maybe Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word8 -> Bool) -> Word8 -> Maybe Word8
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word8
forall a. Bounded a => a
minBound)

instance Finitary Word16 where
  type Cardinality Word16 = $(cardinalityOf @Word16)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Word16) -> Word16
fromFinite = Int -> Word16
forall a. Enum a => Int -> a
toEnum (Int -> Word16) -> (Finite 65536 -> Int) -> Finite 65536 -> Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite 65536 -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE toFinite #-}
  toFinite :: Word16 -> Finite (Cardinality Word16)
toFinite = Int -> Finite 65536
forall a. Enum a => Int -> a
toEnum (Int -> Finite 65536) -> (Word16 -> Int) -> Word16 -> Finite 65536
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word16 -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE start #-}
  start :: (1 <= Cardinality Word16) => Word16
start = Word16
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Word16) => Word16
end = Word16
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word16 -> Maybe Word16
next = (Word16 -> Word16) -> Maybe Word16 -> Maybe Word16
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Word16
forall a. Enum a => a -> a
succ (Maybe Word16 -> Maybe Word16)
-> (Word16 -> Maybe Word16) -> Word16 -> Maybe Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word16 -> Bool) -> Word16 -> Maybe Word16
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word16 -> Word16 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word16
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Word16 -> Maybe Word16
previous = (Word16 -> Word16) -> Maybe Word16 -> Maybe Word16
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Word16
forall a. Enum a => a -> a
pred (Maybe Word16 -> Maybe Word16)
-> (Word16 -> Maybe Word16) -> Word16 -> Maybe Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word16 -> Bool) -> Word16 -> Maybe Word16
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word16 -> Word16 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word16
forall a. Bounded a => a
minBound)

instance Finitary Word32 where
  type Cardinality Word32 = $(cardinalityOf @Word32)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Word32) -> Word32
fromFinite = Finite 4294967296 -> Word32
Finite (Cardinality Word32) -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE toFinite #-}
  toFinite :: Word32 -> Finite (Cardinality Word32)
toFinite = Word32 -> Finite 4294967296
Word32 -> Finite (Cardinality Word32)
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE start #-}
  start :: (1 <= Cardinality Word32) => Word32
start = Word32
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Word32) => Word32
end = Word32
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word32 -> Maybe Word32
next = (Word32 -> Word32) -> Maybe Word32 -> Maybe Word32
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word32 -> Word32
forall a. Num a => a -> a
inc (Maybe Word32 -> Maybe Word32)
-> (Word32 -> Maybe Word32) -> Word32 -> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word32 -> Bool) -> Word32 -> Maybe Word32
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word32
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Word32 -> Maybe Word32
previous = (Word32 -> Word32) -> Maybe Word32 -> Maybe Word32
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word32 -> Word32
forall a. Num a => a -> a
dec (Maybe Word32 -> Maybe Word32)
-> (Word32 -> Maybe Word32) -> Word32 -> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word32 -> Bool) -> Word32 -> Maybe Word32
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word32
forall a. Bounded a => a
minBound)

instance Finitary Word64 where
  type Cardinality Word64 = $(cardinalityOf @Word64)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Word64) -> Word64
fromFinite = Finite 18446744073709551616 -> Word64
Finite (Cardinality Word64) -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE toFinite #-}
  toFinite :: Word64 -> Finite (Cardinality Word64)
toFinite = Word64 -> Finite 18446744073709551616
Word64 -> Finite (Cardinality Word64)
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE start #-}
  start :: (1 <= Cardinality Word64) => Word64
start = Word64
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Word64) => Word64
end = Word64
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word64 -> Maybe Word64
next = (Word64 -> Word64) -> Maybe Word64 -> Maybe Word64
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word64 -> Word64
forall a. Num a => a -> a
inc (Maybe Word64 -> Maybe Word64)
-> (Word64 -> Maybe Word64) -> Word64 -> Maybe Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word64 -> Bool) -> Word64 -> Maybe Word64
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Word64 -> Maybe Word64
previous = (Word64 -> Word64) -> Maybe Word64 -> Maybe Word64
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word64 -> Word64
forall a. Num a => a -> a
dec (Maybe Word64 -> Maybe Word64)
-> (Word64 -> Maybe Word64) -> Word64 -> Maybe Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word64 -> Bool) -> Word64 -> Maybe Word64
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
forall a. Bounded a => a
minBound)

instance Finitary Int8 where
  type Cardinality Int8 = $(cardinalityOf @Int8)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Int8) -> Int8
fromFinite = Int16 -> Int8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int16 -> Int8) -> (Finite 256 -> Int16) -> Finite 256 -> Int8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int16 -> Int16 -> Int16
forall a. Num a => a -> a -> a
subtract Int16
128 (Int16 -> Int16) -> (Finite 256 -> Int16) -> Finite 256 -> Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int16
  {-# INLINE toFinite #-}
  toFinite :: Int8 -> Finite (Cardinality Int8)
toFinite = Int16 -> Finite 256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int16 -> Finite 256) -> (Int8 -> Int16) -> Int8 -> Finite 256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int16 -> Int16 -> Int16
forall a. Num a => a -> a -> a
+ Int16
128) (Int16 -> Int16) -> (Int8 -> Int16) -> Int8 -> Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int16
  {-# INLINE start #-}
  start :: (1 <= Cardinality Int8) => Int8
start = Int8
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Int8) => Int8
end = Int8
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int8 -> Maybe Int8
next = (Int8 -> Int8) -> Maybe Int8 -> Maybe Int8
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int8 -> Int8
forall a. Enum a => a -> a
succ (Maybe Int8 -> Maybe Int8)
-> (Int8 -> Maybe Int8) -> Int8 -> Maybe Int8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int8 -> Bool) -> Int8 -> Maybe Int8
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int8 -> Int8 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int8
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Int8 -> Maybe Int8
previous = (Int8 -> Int8) -> Maybe Int8 -> Maybe Int8
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int8 -> Int8
forall a. Enum a => a -> a
pred (Maybe Int8 -> Maybe Int8)
-> (Int8 -> Maybe Int8) -> Int8 -> Maybe Int8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int8 -> Bool) -> Int8 -> Maybe Int8
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int8 -> Int8 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int8
forall a. Bounded a => a
minBound)

instance Finitary Int16 where
  type Cardinality Int16 = $(cardinalityOf @Int16)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Int16) -> Int16
fromFinite = Int32 -> Int16
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> Int16)
-> (Finite 65536 -> Int32) -> Finite 65536 -> Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
subtract Int32
32768 (Int32 -> Int32)
-> (Finite 65536 -> Int32) -> Finite 65536 -> Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int32
  {-# INLINE toFinite #-}
  toFinite :: Int16 -> Finite (Cardinality Int16)
toFinite = Int32 -> Finite 65536
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> Finite 65536)
-> (Int16 -> Int32) -> Int16 -> Finite 65536
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ Int32
32768) (Int32 -> Int32) -> (Int16 -> Int32) -> Int16 -> Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int32
  {-# INLINE start #-}
  start :: (1 <= Cardinality Int16) => Int16
start = Int16
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Int16) => Int16
end = Int16
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int16 -> Maybe Int16
next = (Int16 -> Int16) -> Maybe Int16 -> Maybe Int16
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int16 -> Int16
forall a. Enum a => a -> a
succ (Maybe Int16 -> Maybe Int16)
-> (Int16 -> Maybe Int16) -> Int16 -> Maybe Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int16 -> Bool) -> Int16 -> Maybe Int16
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int16 -> Int16 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int16
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Int16 -> Maybe Int16
previous = (Int16 -> Int16) -> Maybe Int16 -> Maybe Int16
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int16 -> Int16
forall a. Enum a => a -> a
pred (Maybe Int16 -> Maybe Int16)
-> (Int16 -> Maybe Int16) -> Int16 -> Maybe Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int16 -> Bool) -> Int16 -> Maybe Int16
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int16 -> Int16 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int16
forall a. Bounded a => a
minBound)

instance Finitary Int32 where
  type Cardinality Int32 = $(cardinalityOf @Int32)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Int32) -> Int32
fromFinite = forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int32 (Integer -> Int32)
-> (Finite 4294967296 -> Integer) -> Finite 4294967296 -> Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract $(adjustmentOf @Int32) (Integer -> Integer)
-> (Finite 4294967296 -> Integer) -> Finite 4294967296 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer
  {-# INLINE toFinite #-}
  toFinite :: Int32 -> Finite (Cardinality Int32)
toFinite = Integer -> Finite 4294967296
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Finite 4294967296)
-> (Int32 -> Integer) -> Int32 -> Finite 4294967296
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ $(adjustmentOf @Int32)) (Integer -> Integer) -> (Int32 -> Integer) -> Int32 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer (Int -> Integer) -> (Int32 -> Int) -> Int32 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE start #-}
  start :: (1 <= Cardinality Int32) => Int32
start = Int32
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Int32) => Int32
end = Int32
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int32 -> Maybe Int32
next = (Int32 -> Int32) -> Maybe Int32 -> Maybe Int32
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int32 -> Int32
forall a. Num a => a -> a
inc (Maybe Int32 -> Maybe Int32)
-> (Int32 -> Maybe Int32) -> Int32 -> Maybe Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int32 -> Bool) -> Int32 -> Maybe Int32
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int32
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Int32 -> Maybe Int32
previous = (Int32 -> Int32) -> Maybe Int32 -> Maybe Int32
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int32 -> Int32
forall a. Num a => a -> a
dec (Maybe Int32 -> Maybe Int32)
-> (Int32 -> Maybe Int32) -> Int32 -> Maybe Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int32 -> Bool) -> Int32 -> Maybe Int32
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int32
forall a. Bounded a => a
minBound)

instance Finitary Int64 where
  type Cardinality Int64 = $(cardinalityOf @Int64)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Int64) -> Int64
fromFinite = forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int64 (Integer -> Int64)
-> (Finite 18446744073709551616 -> Integer)
-> Finite 18446744073709551616
-> Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract $(adjustmentOf @Int64) (Integer -> Integer)
-> (Finite 18446744073709551616 -> Integer)
-> Finite 18446744073709551616
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer
  {-# INLINE toFinite #-}
  toFinite :: Int64 -> Finite (Cardinality Int64)
toFinite = Integer -> Finite 18446744073709551616
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Finite 18446744073709551616)
-> (Int64 -> Integer) -> Int64 -> Finite 18446744073709551616
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ $(adjustmentOf @Int64)) (Integer -> Integer) -> (Int64 -> Integer) -> Int64 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer (Int -> Integer) -> (Int64 -> Int) -> Int64 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE start #-}
  start :: (1 <= Cardinality Int64) => Int64
start = Int64
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Int64) => Int64
end = Int64
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int64 -> Maybe Int64
next = (Int64 -> Int64) -> Maybe Int64 -> Maybe Int64
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int64 -> Int64
forall a. Num a => a -> a
inc (Maybe Int64 -> Maybe Int64)
-> (Int64 -> Maybe Int64) -> Int64 -> Maybe Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int64 -> Bool) -> Int64 -> Maybe Int64
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int64
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Int64 -> Maybe Int64
previous = (Int64 -> Int64) -> Maybe Int64 -> Maybe Int64
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int64 -> Int64
forall a. Num a => a -> a
dec (Maybe Int64 -> Maybe Int64)
-> (Int64 -> Maybe Int64) -> Int64 -> Maybe Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int64 -> Bool) -> Int64 -> Maybe Int64
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int64
forall a. Bounded a => a
minBound)

-- 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 :: Finite (Cardinality Int) -> Int
fromFinite = forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int (Integer -> Int)
-> (Finite 18446744073709551616 -> Integer)
-> Finite 18446744073709551616
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract $(adjustmentOf @Int) (Integer -> Integer)
-> (Finite 18446744073709551616 -> Integer)
-> Finite 18446744073709551616
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer
  {-# INLINE toFinite #-}
  toFinite :: Int -> Finite (Cardinality Int)
toFinite = Integer -> Finite 18446744073709551616
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Finite 18446744073709551616)
-> (Int -> Integer) -> Int -> Finite 18446744073709551616
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ $(adjustmentOf @Int)) (Integer -> Integer) -> (Int -> Integer) -> Int -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer (Int -> Integer) -> (Int -> Int) -> Int -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE start #-}
  start :: (1 <= Cardinality Int) => Int
start = Int
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Int) => Int
end = Int
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int -> Maybe Int
next = (Int -> Int) -> Maybe Int -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Int
forall a. Num a => a -> a
inc (Maybe Int -> Maybe Int) -> (Int -> Maybe Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Bool) -> Int -> Maybe Int
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Int -> Maybe Int
previous = (Int -> Int) -> Maybe Int -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Int
forall a. Num a => a -> a
dec (Maybe Int -> Maybe Int) -> (Int -> Maybe Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Bool) -> Int -> Maybe Int
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
forall a. Bounded a => a
minBound)

-- | '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 :: Finite (Cardinality Word) -> Word
fromFinite = Finite 18446744073709551616 -> Word
Finite (Cardinality Word) -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE toFinite #-}
  toFinite :: Word -> Finite (Cardinality Word)
toFinite = Word -> Finite 18446744073709551616
Word -> Finite (Cardinality Word)
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE start #-}
  start :: (1 <= Cardinality Word) => Word
start = Word
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality Word) => Word
end = Word
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word -> Maybe Word
next = (Word -> Word) -> Maybe Word -> Maybe Word
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word -> Word
forall a. Num a => a -> a
inc (Maybe Word -> Maybe Word)
-> (Word -> Maybe Word) -> Word -> Maybe Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word -> Bool) -> Word -> Maybe Word
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
/= Word
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Word -> Maybe Word
previous = (Word -> Word) -> Maybe Word -> Maybe Word
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Word -> Word
forall a. Num a => a -> a
dec (Maybe Word -> Maybe Word)
-> (Word -> Maybe Word) -> Word -> Maybe Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word -> Bool) -> Word -> Maybe Word
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
/= Word
forall a. Bounded a => a
minBound)

-- | 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 :: Finite (Cardinality (Finite n)) -> Finite n
fromFinite = Finite n -> Finite n
Finite (Cardinality (Finite n)) -> Finite n
forall a. a -> a
id
  {-# INLINE toFinite #-}
  toFinite :: Finite n -> Finite (Cardinality (Finite n))
toFinite = Finite n -> Finite n
Finite n -> Finite (Cardinality (Finite n))
forall a. a -> a
id
  {-# INLINE start #-}
  start :: (1 <= Cardinality (Finite n)) => Finite n
start = Finite n
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: (1 <= Cardinality (Finite n)) => Finite n
end = Finite n
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Finite n -> Maybe (Finite n)
next = (Finite n -> Finite n) -> Maybe (Finite n) -> Maybe (Finite n)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Finite n -> Finite n
forall a. Num a => a -> a
inc (Maybe (Finite n) -> Maybe (Finite n))
-> (Finite n -> Maybe (Finite n)) -> Finite n -> Maybe (Finite n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite n -> Bool) -> Finite n -> Maybe (Finite n)
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Finite n -> Finite n -> Bool
forall a. Eq a => a -> a -> Bool
/= Finite n
forall a. Bounded a => a
maxBound)
  {-# INLINE previous #-}
  previous :: Finite n -> Maybe (Finite n)
previous = (Finite n -> Finite n) -> Maybe (Finite n) -> Maybe (Finite n)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Finite n -> Finite n
forall a. Num a => a -> a
dec (Maybe (Finite n) -> Maybe (Finite n))
-> (Finite n -> Maybe (Finite n)) -> Finite n -> Maybe (Finite n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite n -> Bool) -> Finite n -> Maybe (Finite n)
forall a (f :: Type -> Type).
Alternative f =>
(a -> Bool) -> a -> f a
guarded (Finite n -> Finite n -> Bool
forall a. Eq a => a -> a -> Bool
/= Finite n
forall a. Bounded a => a
minBound)

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

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

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)

-- | 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 :: Finite (Cardinality (Down a)) -> Down a
fromFinite = a -> Down a
forall a. a -> Down a
Down (a -> Down a)
-> (Finite (Cardinality a) -> a)
-> Finite (Cardinality a)
-> Down a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality a) -> a)
-> (Finite (Cardinality a) -> Finite (Cardinality a))
-> Finite (Cardinality a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
KnownNat (Cardinality a) =>
Finite (Cardinality a) -> Finite (Cardinality a)
opp @a
  {-# INLINABLE toFinite #-}
  toFinite :: Down a -> Finite (Cardinality (Down a))
toFinite (Down a
x) = forall a.
KnownNat (Cardinality a) =>
Finite (Cardinality a) -> Finite (Cardinality a)
opp @a (Finite (Cardinality a) -> Finite (Cardinality (Down a)))
-> (a -> Finite (Cardinality a))
-> a
-> Finite (Cardinality (Down a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite (a -> Finite (Cardinality (Down a)))
-> a -> Finite (Cardinality (Down a))
forall a b. (a -> b) -> a -> b
$ a
x

#ifdef VECTOR
-- | 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
  {-# INLINABLE fromFinite #-}
  fromFinite :: Finite (Cardinality (Vector n a)) -> Vector n a
fromFinite Finite (Cardinality (Vector n a))
i = (forall s. ST s (Vector n a)) -> Vector n a
forall a. (forall s. ST s a) -> a
runST (Finite (Cardinality (Vector n a)) -> ST s (Vector n a)
forall s. Finite (Cardinality (Vector n a)) -> ST s (Vector n a)
go Finite (Cardinality (Vector n a))
i)
    where
      go :: Finite (Cardinality (VS.Vector n a)) -> ST s (VS.Vector n a)
      go :: forall s. Finite (Cardinality (Vector n a)) -> ST s (Vector n a)
go Finite (Cardinality (Vector n a))
ix = do
        MVector n s a
v <- ST s (MVector n s a)
ST s (MVector n (PrimState (ST s)) a)
forall (n :: Nat) (m :: Type -> Type) a.
(KnownNat n, PrimMonad m) =>
m (MVector n (PrimState m) a)
VMS.new
        MVector n (PrimState (ST s)) a
-> Finite (Cardinality a ^ n) -> ST s ()
forall a (m :: Type -> Type) (v :: Type -> Type -> Type)
       (n :: Nat).
(Finitary a, PrimMonad m, KnownNat n, MVector v a) =>
MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()
unroll MVector n s a
MVector n (PrimState (ST s)) a
v Finite (Cardinality a ^ n)
Finite (Cardinality (Vector n a))
ix
        MVector n (PrimState (ST s)) a -> ST s (Vector n a)
forall (m :: Type -> Type) (n :: Nat) a.
PrimMonad m =>
MVector n (PrimState m) a -> m (Vector n a)
VS.unsafeFreeze MVector n s a
MVector n (PrimState (ST s)) a
v
  {-# INLINE toFinite #-}
  toFinite :: Vector n a -> Finite (Cardinality (Vector n a))
toFinite = Vector n a -> Finite (Cardinality a ^ n)
Vector n a -> Finite (Cardinality (Vector n a))
forall a (v :: Type -> Type) (n :: Nat).
(Finitary a, Vector v a, KnownNat n) =>
Vector v n a -> Finite (Cardinality a ^ n)
roll

instance (Finitary a, VUMS.Unbox a, KnownNat n) => Finitary (VUS.Vector n a) where
  type Cardinality (VUS.Vector n a) = Cardinality a ^ n
  {-# INLINABLE fromFinite #-}
  fromFinite :: Finite (Cardinality (Vector n a)) -> Vector n a
fromFinite Finite (Cardinality (Vector n a))
i = (forall s. ST s (Vector n a)) -> Vector n a
forall a. (forall s. ST s a) -> a
runST (Finite (Cardinality (Vector n a)) -> ST s (Vector n a)
forall s. Finite (Cardinality (Vector n a)) -> ST s (Vector n a)
go Finite (Cardinality (Vector n a))
i)
    where
      go :: Finite (Cardinality (VUS.Vector n a)) -> ST s (VUS.Vector n a)
      go :: forall s. Finite (Cardinality (Vector n a)) -> ST s (Vector n a)
go Finite (Cardinality (Vector n a))
ix = do
        MVector n s a
v <- ST s (MVector n s a)
ST s (MVector n (PrimState (ST s)) a)
forall (n :: Nat) (m :: Type -> Type) a.
(KnownNat n, PrimMonad m, Unbox a) =>
m (MVector n (PrimState m) a)
VUMS.new
        MVector n (PrimState (ST s)) a
-> Finite (Cardinality a ^ n) -> ST s ()
forall a (m :: Type -> Type) (v :: Type -> Type -> Type)
       (n :: Nat).
(Finitary a, PrimMonad m, KnownNat n, MVector v a) =>
MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()
unroll MVector n s a
MVector n (PrimState (ST s)) a
v Finite (Cardinality a ^ n)
Finite (Cardinality (Vector n a))
ix
        MVector n (PrimState (ST s)) a -> ST s (Vector n a)
forall (m :: Type -> Type) a (n :: Nat).
(PrimMonad m, Unbox a) =>
MVector n (PrimState m) a -> m (Vector n a)
VUS.unsafeFreeze MVector n s a
MVector n (PrimState (ST s)) a
v
  {-# INLINE toFinite #-}
  toFinite :: Vector n a -> Finite (Cardinality (Vector n a))
toFinite = Vector n a -> Finite (Cardinality a ^ n)
Vector n a -> Finite (Cardinality (Vector n a))
forall a (v :: Type -> Type) (n :: Nat).
(Finitary a, Vector v a, KnownNat n) =>
Vector v n a -> Finite (Cardinality a ^ n)
roll

instance (Finitary a, Storable a, KnownNat n) => Finitary (VSS.Vector n a) where
  type Cardinality (VSS.Vector n a) = Cardinality a ^ n
  {-# INLINABLE fromFinite #-}
  fromFinite :: Finite (Cardinality (Vector n a)) -> Vector n a
fromFinite Finite (Cardinality (Vector n a))
i = (forall s. ST s (Vector n a)) -> Vector n a
forall a. (forall s. ST s a) -> a
runST (Finite (Cardinality (Vector n a)) -> ST s (Vector n a)
forall s. Finite (Cardinality (Vector n a)) -> ST s (Vector n a)
go Finite (Cardinality (Vector n a))
i)
    where
      go :: Finite (Cardinality (VSS.Vector n a)) -> ST s (VSS.Vector n a)
      go :: forall s. Finite (Cardinality (Vector n a)) -> ST s (Vector n a)
go Finite (Cardinality (Vector n a))
ix = do
        MVector n s a
v <- ST s (MVector n s a)
ST s (MVector n (PrimState (ST s)) a)
forall (n :: Nat) (m :: Type -> Type) a.
(KnownNat n, PrimMonad m, Storable a) =>
m (MVector n (PrimState m) a)
VSMS.new
        MVector n (PrimState (ST s)) a
-> Finite (Cardinality a ^ n) -> ST s ()
forall a (m :: Type -> Type) (v :: Type -> Type -> Type)
       (n :: Nat).
(Finitary a, PrimMonad m, KnownNat n, MVector v a) =>
MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()
unroll MVector n s a
MVector n (PrimState (ST s)) a
v Finite (Cardinality a ^ n)
Finite (Cardinality (Vector n a))
ix
        MVector n (PrimState (ST s)) a -> ST s (Vector n a)
forall (m :: Type -> Type) a (n :: Nat).
(PrimMonad m, Storable a) =>
MVector n (PrimState m) a -> m (Vector n a)
VSS.unsafeFreeze MVector n s a
MVector n (PrimState (ST s)) a
v
  {-# INLINE toFinite #-}
  toFinite :: Vector n a -> Finite (Cardinality (Vector n a))
toFinite = Vector n a -> Finite (Cardinality a ^ n)
Vector n a -> Finite (Cardinality (Vector n a))
forall a (v :: Type -> Type) (n :: Nat).
(Finitary a, Vector v a, KnownNat n) =>
Vector v n a -> Finite (Cardinality a ^ n)
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 :: Type -> Type) (v :: Type -> Type -> Type)
       (n :: Nat).
(Finitary a, PrimMonad m, KnownNat n, MVector v a) =>
MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()
unroll MVector v n (PrimState m) a
v Finite (Cardinality a ^ n)
acc =
  forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ @_ @_ @_ @()
    (Proxy 1 -> Proxy n -> Maybe ((1 <=? n) :~: 'True)
forall (m :: Nat) (n :: Nat) (p :: Nat -> Type) (q :: Nat -> Type).
(KnownNat m, KnownNat n) =>
p m -> q n -> Maybe ((m <=? n) :~: 'True)
isLE (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @1) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
    ( \OrdCond (CmpNat 1 n) 'True 'True 'False :~: 'True
Refl -> do
        let (Finite (Cardinality a ^ (n - 1))
d, Finite (Cardinality a)
r) = forall (n :: Nat) (m :: Nat).
KnownNat n =>
Finite (n * m) -> (Finite n, Finite m)
separateProduct @(Cardinality a ^ (n -1)) @(Cardinality a) Finite ((Cardinality a ^ (n - 1)) * Cardinality a)
Finite (Cardinality a ^ n)
acc
        let x :: a
x = Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite Finite (Cardinality a)
r
        MVector v n (PrimState m) a -> Finite n -> a -> m ()
forall (v :: Type -> Type -> Type) (n :: Nat) (m :: Type -> Type)
       a.
(PrimMonad m, MVector v a) =>
MVector v n (PrimState m) a -> Finite n -> a -> m ()
VGMS.write MVector v n (PrimState m) a
v Finite n
0 a
x
        MVector v (n - 1) (PrimState m) a
-> Finite (Cardinality a ^ (n - 1)) -> m ()
forall a (m :: Type -> Type) (v :: Type -> Type -> Type)
       (n :: Nat).
(Finitary a, PrimMonad m, KnownNat n, MVector v a) =>
MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()
unroll (MVector v (1 + (n - 1)) (PrimState m) a
-> MVector v (n - 1) (PrimState m) a
forall (v :: Type -> Type -> Type) (n :: Nat) s a.
MVector v a =>
MVector v (1 + n) s a -> MVector v n s a
VGMS.tail MVector v n (PrimState m) a
MVector v (1 + (n - 1)) (PrimState m) a
v) Finite (Cardinality a ^ (n - 1))
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 :: Type -> Type) (n :: Nat).
(Finitary a, Vector v a, KnownNat n) =>
Vector v n a -> Finite (Cardinality a ^ n)
roll Vector v n a
v = case Proxy 1 -> Proxy n -> Maybe ((1 <=? n) :~: 'True)
forall (m :: Nat) (n :: Nat) (p :: Nat -> Type) (q :: Nat -> Type).
(KnownNat m, KnownNat n) =>
p m -> q n -> Maybe ((m <=? n) :~: 'True)
isLE (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @1) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) of
  Maybe ((1 <=? n) :~: 'True)
Nothing -> Finite (Cardinality a ^ n)
0
  Just (1 <=? n) :~: 'True
Refl ->
    let (a
h, Vector v (n - 1) a
t) = (Vector v (1 + (n - 1)) a -> a
forall (v :: Type -> Type) (n :: Nat) a.
Vector v a =>
Vector v (1 + n) a -> a
VGS.head Vector v n a
Vector v (1 + (n - 1)) a
v, Vector v (1 + (n - 1)) a -> Vector v (n - 1) a
forall (v :: Type -> Type) (n :: Nat) a.
Vector v a =>
Vector v (1 + n) a -> Vector v n a
VGS.tail Vector v n a
Vector v (1 + (n - 1)) a
v)
     in (Finite (Cardinality a ^ (n - 1)), Finite (Cardinality a))
-> Finite ((Cardinality a ^ (n - 1)) * Cardinality a)
forall (n :: Nat) (m :: Nat).
KnownNat n =>
(Finite n, Finite m) -> Finite (n * m)
combineProduct (Vector v (n - 1) a -> Finite (Cardinality a ^ (n - 1))
forall a (v :: Type -> Type) (n :: Nat).
(Finitary a, Vector v a, KnownNat n) =>
Vector v n a -> Finite (Cardinality a ^ n)
roll Vector v (n - 1) a
t, a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite a
h)
#endif

-- * Enumeration helpers


-- | Produce every inhabitant of @a@, in ascending order of indexes.

-- If you want descending order, use @Down a@ instead.

{-# INLINE inhabitants #-}
inhabitants :: forall (a :: Type). (Finitary a) => [a]
inhabitants :: forall a. Finitary a => [a]
inhabitants = Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality a) -> a) -> [Finite (Cardinality a)] -> [a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Finite (Cardinality a)]
forall (n :: Nat). KnownNat n => [Finite n]
finites

-- | Produce every inhabitant of @a@, starting with the argument, in ascending

-- order of indexes.

-- If you want descending order, use @Down a@ instead.

{-# INLINABLE inhabitantsFrom #-}
inhabitantsFrom :: forall (a :: Type). (Finitary a) => a -> NonEmpty a
inhabitantsFrom :: forall a. Finitary a => a -> NonEmpty a
inhabitantsFrom a
x = a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap @Maybe ((Finite (Cardinality a) -> a) -> [Finite (Cardinality a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite ([Finite (Cardinality a)] -> [a])
-> (a -> [Finite (Cardinality a)]) -> a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality a) -> [Finite (Cardinality a)]
forall a. Enum a => a -> [a]
enumFrom (Finite (Cardinality a) -> [Finite (Cardinality a)])
-> (a -> Finite (Cardinality a)) -> a -> [Finite (Cardinality a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite) (a -> Maybe a
forall a. Finitary a => a -> Maybe a
next a
x)

-- | Produce every inhabitant of @a@, up to and including the argument, in

-- ascending order of indexes.

-- If you want descending order, use @Down a@ instead.

{-# INLINABLE inhabitantsTo #-}
inhabitantsTo :: forall (a :: Type). (Finitary a) => a -> NonEmpty a
inhabitantsTo :: forall a. Finitary a => a -> NonEmpty a
inhabitantsTo a
x = [a] -> NonEmpty a
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList (Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality a) -> a) -> [Finite (Cardinality a)] -> [a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Finite (Cardinality a)
0 .. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite a
x])

-- | Produce every inhabitant of @a@, starting with the first argument, up to

-- the second argument, in ascending order of indexes. @inhabitantsFromTo x y@

-- will produce the empty list if @toFinite x > toFinite y@.

-- If you want descending order, use @Down a@ instead.

{-# INLINABLE inhabitantsFromTo #-}
inhabitantsFromTo :: forall (a :: Type). (Finitary a) => a -> a -> [a]
inhabitantsFromTo :: forall a. Finitary a => a -> a -> [a]
inhabitantsFromTo a
lo a
hi = Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality a) -> a) -> [Finite (Cardinality a)] -> [a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite a
lo .. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite a
hi]

-- Helpers


{-# INLINABLE combineProduct' #-}
combineProduct' :: forall n m. (KnownNat m) => (Finite n, Finite m) -> Finite (n * m)
combineProduct' :: forall (n :: Nat) (m :: Nat).
KnownNat m =>
(Finite n, Finite m) -> Finite (n * m)
combineProduct' ( Finite Integer
i, Finite Integer
j ) = Integer -> Finite Integer (n * m)
forall a (n :: Nat). a -> Finite a n
Finite ( Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j )
  where
    m :: Integer
    m :: Integer
m = Nat -> Integer
forall a. Integral a => a -> Integer
toInteger ( forall (n :: Nat). KnownNat n => Proxy# n -> Nat
natVal' @m Proxy# m
forall {k} (a :: k). Proxy# a
proxy# )

{-# INLINABLE separateProduct' #-}
separateProduct' :: forall n m. (KnownNat m) => Finite (n * m) -> (Finite n, Finite m)
separateProduct' :: forall (n :: Nat) (m :: Nat).
KnownNat m =>
Finite (n * m) -> (Finite n, Finite m)
separateProduct' ( Finite Integer
a ) = ( Integer -> Finite Integer n
forall a (n :: Nat). a -> Finite a n
Finite Integer
q, Integer -> Finite Integer m
forall a (n :: Nat). a -> Finite a n
Finite Integer
r )
  where
    m, q, r :: Integer
    m :: Integer
m = Nat -> Integer
forall a. Integral a => a -> Integer
toInteger ( forall (n :: Nat). KnownNat n => Proxy# n -> Nat
natVal' @m Proxy# m
forall {k} (a :: k). Proxy# a
proxy# )
    ( Integer
q, Integer
r ) = Integer
a Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`quotRem` Integer
m

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

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

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

{-# INLINE opp #-}
opp :: forall a. (KnownNat (Cardinality a)) => Finite (Cardinality a) -> Finite (Cardinality a)
opp :: forall a.
KnownNat (Cardinality a) =>
Finite (Cardinality a) -> Finite (Cardinality a)
opp = ( Finite (Cardinality a)
forall a. Bounded a => a
maxBound Finite (Cardinality a)
-> Finite (Cardinality a) -> Finite (Cardinality a)
forall a. Num a => a -> a -> a
- )