{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoStarIsType #-}
{-# 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
-- Maintainer:    koz.ross@retro-freedom.nz
-- 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

import Control.Applicative (Alternative (..), Const)
import Control.Monad (forM_, join)
import Control.Monad.Primitive (PrimMonad (..))
import Control.Monad.ST (ST, runST)
import Data.Bifunctor (bimap, first)
import qualified Data.Bit as B
import qualified Data.Bit.ThreadSafe as BTS
import Data.Bool (bool)
import Data.Finitary.TH
import Data.Finite
  ( Finite,
    combineProduct,
    finites,
    separateProduct,
    separateSum,
    shiftN,
    weakenN,
  )
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.Type.Equality ((:~:) (..))
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Generic.Mutable as VGM
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
import Data.Void (Void)
import Data.Word (Word16, Word32, Word64, Word8)
import Foreign.Storable (Storable)
import GHC.Generics
  ( (:*:) (..),
    (:+:) (..),
    Generic,
    K1 (..),
    M1 (..),
    Rep,
    U1 (..),
    V1,
    from,
    to,
  )
import GHC.TypeLits.Compare (isLE)
import GHC.TypeNats
import Numeric.Natural (Natural)

-- | 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
to (Rep a Any -> a)
-> (Finite (Cardinality a) -> Rep a Any)
-> Finite (Cardinality a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality a) -> Rep a Any
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 (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 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 (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 (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
. Finite (Cardinality a) -> Finite (Cardinality a)
forall a. Num a => a -> a
dec (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

  -- | @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 (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 (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
. Finite (Cardinality a) -> Finite (Cardinality a)
forall a. Num a => a -> a
inc (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

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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 i c k (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 :: 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 (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 (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
  {-# INLINE gToFinite #-}
  gToFinite :: (:+:) a b x -> Finite (GCardinality (a :+: b))
gToFinite (L1 a x
x) = Finite (GCardinality a) -> Finite (GCardinality a + GCardinality b)
forall (n :: Nat) (m :: Nat). (n <= m) => Finite n -> Finite m
weakenN (Finite (GCardinality a)
 -> Finite (GCardinality a + GCardinality b))
-> (a x -> Finite (GCardinality a))
-> a x
-> Finite (GCardinality a + GCardinality b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a x -> Finite (GCardinality a)
forall (a :: Type -> Type) x.
GFinitary a =>
a x -> Finite (GCardinality a)
gToFinite (a x -> Finite (GCardinality a + GCardinality b))
-> a x -> Finite (GCardinality a + GCardinality b)
forall a b. (a -> b) -> a -> b
$ a x
x
  gToFinite (R1 b x
x) = Finite (GCardinality b) -> Finite (GCardinality a + GCardinality b)
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m, n <= m) =>
Finite n -> Finite m
shiftN (Finite (GCardinality b)
 -> Finite (GCardinality a + GCardinality b))
-> (b x -> Finite (GCardinality b))
-> b x
-> Finite (GCardinality a + GCardinality b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b x -> Finite (GCardinality b)
forall (a :: Type -> Type) x.
GFinitary a =>
a x -> Finite (GCardinality a)
gToFinite (b x -> Finite (GCardinality a + GCardinality b))
-> b x -> Finite (GCardinality a + GCardinality 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
  {-# INLINE gFromFinite #-}
  gFromFinite :: 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 n, 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 (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 (a :: Type -> Type) x.
GFinitary a =>
Finite (GCardinality a) -> a x
gFromFinite Finite (GCardinality b)
y
  {-# INLINE gToFinite #-}
  gToFinite :: (:*:) a b x -> Finite (GCardinality (a :*: b))
gToFinite (a x
x :*: b x
y) = (Finite (GCardinality a), Finite (GCardinality b))
-> Finite (GCardinality a * GCardinality b)
forall (n :: Nat) (m :: Nat).
(KnownNat n, 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 (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 (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 :: 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 (a :: Type -> Type) x.
GFinitary a =>
Finite (GCardinality a) -> a x
gFromFinite
  {-# INLINE gToFinite #-}
  gToFinite :: M1 _x _y a x -> Finite (GCardinality (M1 _x _y a))
gToFinite = 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 i (c :: Meta) k (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

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 :: Bit
start = Bit
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Bit
end = Bit
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Bit -> Maybe Bit
next = (Bit -> Bit) -> Maybe Bit -> Maybe Bit
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 (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 :: Bit
start = Bit
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Bit
end = Bit
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Bit -> Maybe Bit
next = (Bit -> Bit) -> Maybe Bit -> Maybe Bit
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 (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 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 :: Char
start = Char
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Char
end = Char
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Char -> Maybe Char
next = (Char -> Char) -> Maybe Char -> Maybe Char
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 (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 :: Word8
start = Word8
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Word8
end = Word8
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word8 -> Maybe Word8
next = (Word8 -> Word8) -> Maybe Word8 -> Maybe Word8
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 (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 :: Word16
start = Word16
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Word16
end = Word16
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word16 -> Maybe Word16
next = (Word16 -> Word16) -> Maybe Word16 -> Maybe Word16
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 (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 (Cardinality Word32) -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE toFinite #-}
  toFinite :: Word32 -> Finite (Cardinality Word32)
toFinite = Word32 -> Finite (Cardinality Word32)
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE start #-}
  start :: Word32
start = Word32
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Word32
end = Word32
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word32 -> Maybe Word32
next = (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) (Word32 -> Maybe Word32)
-> (Word32 -> Word32) -> Word32 -> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Word32
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Word32 -> Maybe Word32
previous = (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) (Word32 -> Maybe Word32)
-> (Word32 -> Word32) -> Word32 -> Maybe Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Word32
forall a. Num a => a -> a
dec

instance Finitary Word64 where
  type Cardinality Word64 = $(cardinalityOf @Word64)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Word64) -> Word64
fromFinite = Finite (Cardinality Word64) -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE toFinite #-}
  toFinite :: Word64 -> Finite (Cardinality Word64)
toFinite = Word64 -> Finite (Cardinality Word64)
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE start #-}
  start :: Word64
start = Word64
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Word64
end = Word64
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word64 -> Maybe Word64
next = (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) (Word64 -> Maybe Word64)
-> (Word64 -> Word64) -> Word64 -> Maybe Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Word64
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Word64 -> Maybe Word64
previous = (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) (Word64 -> Maybe Word64)
-> (Word64 -> Word64) -> Word64 -> Maybe Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Word64
forall a. Num a => a -> a
dec

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
. (Integral (Finite 256), Num Int16) => Finite 256 -> Int16
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
. (Integral Int8, Num Int16) => Int8 -> Int16
forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int16
  {-# INLINE start #-}
  start :: Int8
start = Int8
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Int8
end = Int8
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int8 -> Maybe Int8
next = (Int8 -> Int8) -> Maybe Int8 -> Maybe Int8
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 (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
. (Integral (Finite 65536), Num Int32) => Finite 65536 -> Int32
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
. (Integral Int16, Num Int32) => Int16 -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Int32
  {-# INLINE start #-}
  start :: Int16
start = Int16
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Int16
end = Int16
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int16 -> Maybe Int16
next = (Int16 -> Int16) -> Maybe Int16 -> Maybe Int16
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 (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 = (Integral Integer, Num Int32) => Integer -> Int32
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
. (Integral (Finite 4294967296), Num Integer) =>
Finite 4294967296 -> Integer
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
. (Integral Int, Num Integer) => Int -> Integer
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 :: Int32
start = Int32
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Int32
end = Int32
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int32 -> Maybe Int32
next = (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) (Int32 -> Maybe Int32) -> (Int32 -> Int32) -> Int32 -> Maybe Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> Int32
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Int32 -> Maybe Int32
previous = (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) (Int32 -> Maybe Int32) -> (Int32 -> Int32) -> Int32 -> Maybe Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> Int32
forall a. Num a => a -> a
dec

instance Finitary Int64 where
  type Cardinality Int64 = $(cardinalityOf @Int64)
  {-# INLINE fromFinite #-}
  fromFinite :: Finite (Cardinality Int64) -> Int64
fromFinite = (Integral Integer, Num Int64) => Integer -> Int64
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
. (Integral (Finite 18446744073709551616), Num Integer) =>
Finite 18446744073709551616 -> Integer
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
. (Integral Int, Num Integer) => Int -> Integer
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 :: Int64
start = Int64
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Int64
end = Int64
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int64 -> Maybe Int64
next = (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) (Int64 -> Maybe Int64) -> (Int64 -> Int64) -> Int64 -> Maybe Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Int64
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Int64 -> Maybe Int64
previous = (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) (Int64 -> Maybe Int64) -> (Int64 -> Int64) -> Int64 -> Maybe Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Int64
forall a. Num a => a -> a
dec

-- 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 = (Integral Integer, Num Int) => Integer -> Int
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
. (Integral (Finite 18446744073709551616), Num Integer) =>
Finite 18446744073709551616 -> Integer
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
. (Integral Int, Num Integer) => Int -> Integer
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 :: Int
start = Int
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Int
end = Int
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Int -> Maybe Int
next = (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) (Int -> Maybe Int) -> (Int -> Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Int -> Maybe Int
previous = (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) (Int -> Maybe Int) -> (Int -> Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Num a => a -> a
dec

-- | '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 (Cardinality Word) -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE toFinite #-}
  toFinite :: Word -> Finite (Cardinality Word)
toFinite = Word -> Finite (Cardinality Word)
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE start #-}
  start :: Word
start = Word
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Word
end = Word
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Word -> Maybe Word
next = (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) (Word -> Maybe Word) -> (Word -> Word) -> Word -> Maybe Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> Word
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Word -> Maybe Word
previous = (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) (Word -> Maybe Word) -> (Word -> Word) -> Word -> Maybe Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> Word
forall a. Num a => a -> a
dec

-- | 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 (Cardinality (Finite n)) -> Finite n
forall a. a -> a
id
  {-# INLINE toFinite #-}
  toFinite :: Finite n -> Finite (Cardinality (Finite n))
toFinite = Finite n -> Finite (Cardinality (Finite n))
forall a. a -> a
id
  {-# INLINE start #-}
  start :: Finite n
start = Finite n
forall a. Bounded a => a
minBound
  {-# INLINE end #-}
  end :: Finite n
end = Finite n
forall a. Bounded a => a
maxBound
  {-# INLINE next #-}
  next :: Finite n -> Maybe (Finite n)
next = (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) (Finite n -> Maybe (Finite n))
-> (Finite n -> Finite n) -> Finite n -> Maybe (Finite n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Finite n
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Finite n -> Maybe (Finite n)
previous = (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) (Finite n -> Maybe (Finite n))
-> (Finite n -> Finite n) -> Finite n -> Maybe (Finite n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Finite n
forall a. Num a => a -> a
dec

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

-- | A fixed-length vector over a type @a@ with an instance of @Finitary@ can be
-- thought of as a fixed-length word over an alphabet of size @Cardinality a@.
-- Since there are only finitely-many of these, we can index them in lex order,
-- with the ordering determined by the @Finitary a@ instance (thus, the
-- \'first\' such @Vector@ is the one where each element is @start :: a@, and
-- the \'last\' is the one where each element is @end :: a@).
instance (Finitary a, KnownNat n) => Finitary (VS.Vector n a) where
  type Cardinality (VS.Vector n a) = Cardinality a ^ n
  {-# INLINE fromFinite #-}
  fromFinite :: 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 :: 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)
forall (n :: Nat) (m :: Type -> Type) a.
(KnownNat n, PrimMonad m) =>
m (MVector n (PrimState m) a)
VMS.new
        MVector 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 MVector n (PrimState (ST s)) a
v Finite (Cardinality a ^ n)
Finite (Cardinality (Vector n a))
ix
        MVector 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 MVector n (PrimState (ST s)) a
v
  {-# INLINE toFinite #-}
  toFinite :: Vector n a -> Finite (Cardinality (Vector n a))
toFinite = 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
  {-# INLINE 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 :: 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)
forall (n :: Nat) (m :: Type -> Type) a.
(KnownNat n, PrimMonad m, Unbox a) =>
m (MVector n (PrimState m) a)
VUMS.new
        MVector 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 MVector n (PrimState (ST s)) a
v Finite (Cardinality a ^ n)
Finite (Cardinality (Vector n a))
ix
        MVector 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 MVector n (PrimState (ST s)) a
v
  {-# INLINE toFinite #-}
  toFinite :: Vector n a -> Finite (Cardinality (Vector n a))
toFinite = 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
  {-# INLINE 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 :: 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)
forall (n :: Nat) (m :: Type -> Type) a.
(KnownNat n, PrimMonad m, Storable a) =>
m (MVector n (PrimState m) a)
VSMS.new
        MVector 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 MVector n (PrimState (ST s)) a
v Finite (Cardinality a ^ n)
Finite (Cardinality (Vector n a))
ix
        MVector 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 MVector n (PrimState (ST s)) a
v
  {-# INLINE toFinite #-}
  toFinite :: Vector n a -> Finite (Cardinality (Vector n a))
toFinite = 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

-- * 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 :: [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.
{-# INLINE inhabitantsFrom #-}
inhabitantsFrom :: forall (a :: Type). (Finitary a) => a -> NonEmpty a
inhabitantsFrom :: a -> NonEmpty a
inhabitantsFrom a
x = a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| (a -> [a]) -> Maybe a -> [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 (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.
{-# INLINE inhabitantsTo #-}
inhabitantsTo :: forall (a :: Type). (Finitary a) => a -> NonEmpty a
inhabitantsTo :: a -> NonEmpty a
inhabitantsTo a
x = [a] -> NonEmpty a
forall a. [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.
{-# INLINE inhabitantsFromTo #-}
inhabitantsFromTo :: forall (a :: Type). (Finitary a) => a -> a -> [a]
inhabitantsFromTo :: 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

{-# INLINE combineProduct' #-}
combineProduct' :: forall n m. (KnownNat n, KnownNat m) => (Finite n, Finite m) -> Finite (n * m)
combineProduct' :: (Finite n, Finite m) -> Finite (n * m)
combineProduct' = Natural -> Finite (n * m)
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Finite (n * m))
-> ((Finite n, Finite m) -> Natural)
-> (Finite n, Finite m)
-> Finite (n * m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural) -> (Natural, Natural) -> Natural
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(+) ((Natural, Natural) -> Natural)
-> ((Finite n, Finite m) -> (Natural, Natural))
-> (Finite n, Finite m)
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural) -> (Natural, Natural) -> (Natural, Natural)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Proxy m -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal (Proxy m -> Natural) -> Proxy m -> Natural
forall a b. (a -> b) -> a -> b
$ Proxy m
forall k (t :: k). Proxy t
Proxy @m) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
*) ((Natural, Natural) -> (Natural, Natural))
-> ((Finite n, Finite m) -> (Natural, Natural))
-> (Finite n, Finite m)
-> (Natural, Natural)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite n -> Natural)
-> (Finite m -> Natural)
-> (Finite n, Finite m)
-> (Natural, Natural)
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap @_ @_ @Natural @_ @Natural Finite n -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Finite m -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral

{-# INLINE separateProduct' #-}
separateProduct' :: forall n m. (KnownNat n, KnownNat m) => Finite (n * m) -> (Finite n, Finite m)
separateProduct' :: Finite (n * m) -> (Finite n, Finite m)
separateProduct' = (Finite (n * m) -> Finite n)
-> (Finite (n * m) -> Finite m)
-> (Finite (n * m), Finite (n * m))
-> (Finite n, Finite m)
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Natural -> Finite n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Finite n)
-> (Finite (n * m) -> Natural) -> Finite (n * m) -> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\Finite (n * m)
x -> Finite (n * m) -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Finite (n * m)
x Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Proxy m -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal @m Proxy m
forall k (t :: k). Proxy t
Proxy)) (Natural -> Finite m
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Finite m)
-> (Finite (n * m) -> Natural) -> Finite (n * m) -> Finite m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\Finite (n * m)
x -> Finite (n * m) -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Finite (n * m)
x Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Proxy m -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal @m Proxy m
forall k (t :: k). Proxy t
Proxy)) ((Finite (n * m), Finite (n * m)) -> (Finite n, Finite m))
-> (Finite (n * m) -> (Finite (n * m), Finite (n * m)))
-> Finite (n * m)
-> (Finite n, Finite m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite (n * m)
 -> Finite (n * m) -> (Finite (n * m), Finite (n * m)))
-> Finite (n * m) -> (Finite (n * m), Finite (n * m))
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (,)

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 :: MVector v n (PrimState m) a -> Finite (Cardinality a ^ n) -> m ()
unroll MVector v n (PrimState m) a
v Finite (Cardinality a ^ n)
acc =
  Maybe ((1 <=? n) :~: 'True)
-> (((1 <=? n) :~: 'True) -> m ()) -> m ()
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 (Proxy 1
forall k (t :: k). Proxy t
Proxy @1) (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
    ( \(1 <=? n) :~: 'True
Refl -> do
        let (Finite (Cardinality a ^ (n - 1))
d, Finite (Cardinality a)
r) = Finite ((Cardinality a ^ (n - 1)) * Cardinality a)
-> (Finite (Cardinality a ^ (n - 1)), Finite (Cardinality a))
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 :: 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 (Proxy 1
forall k (t :: k). Proxy t
Proxy @1) (Proxy n
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)

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

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

{-# INLINE guarded #-}
guarded :: forall (a :: Type) (f :: Type -> Type). (Alternative f) => (a -> Bool) -> a -> f a
guarded :: (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 (f :: Type -> Type) a. Alternative f => f a
empty (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 :: Finite (Cardinality a) -> Finite (Cardinality a)
opp = (Integral Natural, Num (Finite (Cardinality a))) =>
Natural -> Finite (Cardinality a)
forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @(Finite (Cardinality a)) (Natural -> Finite (Cardinality a))
-> (Finite (Cardinality a) -> Natural)
-> Finite (Cardinality a)
-> Finite (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
n) (Natural -> Natural)
-> (Finite (Cardinality a) -> Natural)
-> Finite (Cardinality a)
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)) (Natural -> Natural)
-> (Finite (Cardinality a) -> Natural)
-> Finite (Cardinality a)
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Natural
forall a. Num a => a -> a
inc (Natural -> Natural)
-> (Finite (Cardinality a) -> Natural)
-> Finite (Cardinality a)
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integral (Finite (Cardinality a)), Num Natural) =>
Finite (Cardinality a) -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Natural
  where
    n :: Natural
n = Proxy (Cardinality a) -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal @(Cardinality a) Proxy (Cardinality a)
forall k (t :: k). Proxy t
Proxy