{-
 - Copyright (C) 2019  Koz Ross <koz.ross@retro-freedom.nz>
 -
 - This program is free software: you can redistribute it and/or modify
 - it under the terms of the GNU General Public License as published by
 - the Free Software Foundation, either version 3 of the License, or
 - (at your option) any later version.
 -
 - This program is distributed in the hope that it will be useful,
 - but WITHOUT ANY WARRANTY; without even the implied warranty of
 - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 - GNU General Public License for more details.
 -
 - You should have received a copy of the GNU General Public License
 - along with this program.  If not, see <http://www.gnu.org/licenses/>.
 -}

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

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

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

-- | 
-- Module:        Data.Finitary
-- Description:   A type class witnessing that a type has finite cardinality.
-- Copyright:     (C) Koz Ross, 2019
-- License:       GPL version 3.0 or later
-- Maintainer:    koz.ross@retro-freedom.nz
-- Stability:     Experimental
-- Portability:   GHC only
--
-- This package provides the 'Finitary' type class, 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 #-}
-- >
-- > import GHC.Generics
-- > import Data.Word
-- >
-- > data Foo = Bar | Baz (Word8, Word8) | Quux Word16
-- >    deriving (Eq, Generic, Finitary)
--
-- This is the easiest method, and also the safest, as GHC will automatically
-- determine the cardinality of @Foo@, as well as defining law-abiding methods.
-- 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 Data.List.NonEmpty (NonEmpty(..))
import Data.Bifunctor (bimap, first)
import Numeric.Natural (Natural)
import Data.Semigroup (Max, Min, Sum, Product, Dual, Last, First, Any, All)
import Data.Functor.Identity (Identity)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Word (Word8, Word16, Word32, Word64)
import Data.Proxy (Proxy(..))
import Data.Void (Void)
import Data.Bool (bool)
import CoercibleUtils (op)
import GHC.Generics (Generic, Rep, U1(..), K1(..), V1, (:+:)(..), (:*:)(..), M1(..), from, to)
import Control.Applicative (Alternative(..), Const)
import Data.Kind (Type)
import GHC.TypeNats
import Data.Finite (Finite, finites, separateSum, separateProduct, combineProduct, weakenN, shiftN)
import Data.Ord (Down(..))
import Control.Monad.Primitive (PrimMonad(..))
import Control.Monad (forM_, join)
import GHC.TypeLits.Compare (isLE)
import Data.Type.Equality ((:~:)(..))
import Control.Monad.ST (ST, runST)
import Foreign.Storable (Storable)

import qualified Data.List.NonEmpty as NE
import qualified Data.Bit as B
import qualified Data.Bit.ThreadSafe as BTS
import qualified Data.Vector.Sized as VS
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Mutable.Sized as VMS
import qualified Data.Vector.Generic.Sized as VGS
import qualified Data.Vector.Generic.Mutable as VGM
import qualified Data.Vector.Generic.Mutable.Sized as VGMS
import qualified Data.Vector.Unboxed.Sized as VUS
import qualified Data.Vector.Unboxed.Mutable.Sized as VUMS
import qualified Data.Vector.Storable.Sized as VSS
import qualified Data.Vector.Storable.Mutable.Sized as VSMS

import Data.Finitary.TH

-- | Witnesses an isomorphism between @a@ and 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} = \texttt{fromFinite} \; \texttt{minBound} \]
--    * \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; \texttt{maxBound} \]
--    * \[ \forall x :: a \; \texttt{end} \neq x \rightarrow \texttt{next} \; x =
-- (\texttt{fromFinite} \circ + 1 \circ \texttt{toFinite}) \; x \]
--    * \[ \forall x :: a \; \texttt{start} \neq x \rightarrow \texttt{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 the inhabitant whose index precedes the index of @x@,
  -- or 'empty' if no such index exists.
  previous :: (Alternative f) => a -> f a
  previous = (Finite (Cardinality a) -> a) -> f (Finite (Cardinality a)) -> f 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 (f (Finite (Cardinality a)) -> f a)
-> (a -> f (Finite (Cardinality a))) -> a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite (Cardinality a) -> Bool)
-> Finite (Cardinality a) -> f (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) -> f (Finite (Cardinality a)))
-> (a -> Finite (Cardinality a)) -> a -> f (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 the inhabitant whose index follows the index of @x@, or
  -- 'empty' if no such index exists.
  next :: (Alternative f) => a -> f a
  next = (Finite (Cardinality a) -> a) -> f (Finite (Cardinality a)) -> f 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 (f (Finite (Cardinality a)) -> f a)
-> (a -> f (Finite (Cardinality a))) -> a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite (Cardinality a) -> Bool)
-> Finite (Cardinality a) -> f (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) -> f (Finite (Cardinality a)))
-> (a -> Finite (Cardinality a)) -> a -> f (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 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
. (a -> K1 _1 a x) -> K1 _1 a x -> a
forall a b (to :: Type -> Type -> Type).
Coercible a b =>
to a b -> b -> a
op a -> K1 _1 a x
forall k i c (p :: k). c -> K1 i c p
K1

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 x :: 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 :+: b)))
-> a x -> Finite (GCardinality (a :+: b))
forall a b. (a -> b) -> a -> b
$ a x
x
  gToFinite (R1 x :: 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 :+: 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
  {-# INLINE gFromFinite #-}
  gFromFinite :: Finite (GCardinality (a :*: b)) -> (:*:) a b x
gFromFinite i :: Finite (GCardinality (a :*: b))
i = let (x :: Finite (GCardinality a)
x, y :: 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 (x :: a x
x :*: y :: 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
. (a x -> M1 _x _y a x) -> M1 _x _y a x -> a x
forall a b (to :: Type -> Type -> Type).
Coercible a b =>
to a b -> b -> a
op 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

-- * 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
. (Bool -> Bit) -> Bit -> Bool
forall a b (to :: Type -> Type -> Type).
Coercible a b =>
to a b -> b -> a
op Bool -> Bit
B.Bit
  {-# 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 -> f Bit
next = (Bit -> Bit) -> f Bit -> f 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 (f Bit -> f Bit) -> (Bit -> f Bit) -> Bit -> f Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Bool) -> Bit -> f 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 -> f Bit
previous = (Bit -> Bit) -> f Bit -> f 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 (f Bit -> f Bit) -> (Bit -> f Bit) -> Bit -> f Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Bool) -> Bit -> f 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
. (Bool -> Bit) -> Bit -> Bool
forall a b (to :: Type -> Type -> Type).
Coercible a b =>
to a b -> b -> a
op Bool -> Bit
BTS.Bit
  {-# 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 -> f Bit
next = (Bit -> Bit) -> f Bit -> f 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 (f Bit -> f Bit) -> (Bit -> f Bit) -> Bit -> f Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Bool) -> Bit -> f 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 -> f Bit
previous = (Bit -> Bit) -> f Bit -> f 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 (f Bit -> f Bit) -> (Bit -> f Bit) -> Bit -> f Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bit -> Bool) -> Bit -> f 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 -> f Char
next = (Char -> Char) -> f Char -> f 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 (f Char -> f Char) -> (Char -> f Char) -> Char -> f Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> Char -> f 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 -> f Char
previous = (Char -> Char) -> f Char -> f 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 (f Char -> f Char) -> (Char -> f Char) -> Char -> f Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> Char -> f 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 -> f Word8
next = (Word8 -> Word8) -> f Word8 -> f 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 (f Word8 -> f Word8) -> (Word8 -> f Word8) -> Word8 -> f Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word8 -> Bool) -> Word8 -> f 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 -> f Word8
previous = (Word8 -> Word8) -> f Word8 -> f 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 (f Word8 -> f Word8) -> (Word8 -> f Word8) -> Word8 -> f Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word8 -> Bool) -> Word8 -> f 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 -> f Word16
next = (Word16 -> Word16) -> f Word16 -> f 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 (f Word16 -> f Word16)
-> (Word16 -> f Word16) -> Word16 -> f Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word16 -> Bool) -> Word16 -> f 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 -> f Word16
previous = (Word16 -> Word16) -> f Word16 -> f 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 (f Word16 -> f Word16)
-> (Word16 -> f Word16) -> Word16 -> f Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word16 -> Bool) -> Word16 -> f 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 -> f Word32
next = (Word32 -> Bool) -> Word32 -> f 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 -> f Word32) -> (Word32 -> Word32) -> Word32 -> f Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Word32
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Word32 -> f Word32
previous = (Word32 -> Bool) -> Word32 -> f 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 -> f Word32) -> (Word32 -> Word32) -> Word32 -> f 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 -> f Word64
next = (Word64 -> Bool) -> Word64 -> f 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 -> f Word64) -> (Word64 -> Word64) -> Word64 -> f Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Word64
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Word64 -> f Word64
previous = (Word64 -> Bool) -> Word64 -> f 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 -> f Word64) -> (Word64 -> Word64) -> Word64 -> f 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 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
+ 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 -> f Int8
next = (Int8 -> Int8) -> f Int8 -> f 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 (f Int8 -> f Int8) -> (Int8 -> f Int8) -> Int8 -> f Int8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int8 -> Bool) -> Int8 -> f 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 -> f Int8
previous = (Int8 -> Int8) -> f Int8 -> f 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 (f Int8 -> f Int8) -> (Int8 -> f Int8) -> Int8 -> f Int8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int8 -> Bool) -> Int8 -> f 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 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
+ 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 -> f Int16
next = (Int16 -> Int16) -> f Int16 -> f 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 (f Int16 -> f Int16) -> (Int16 -> f Int16) -> Int16 -> f Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int16 -> Bool) -> Int16 -> f 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 -> f Int16
previous = (Int16 -> Int16) -> f Int16 -> f 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 (f Int16 -> f Int16) -> (Int16 -> f Int16) -> Int16 -> f Int16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int16 -> Bool) -> Int16 -> f 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 -> f Int32
next = (Int32 -> Bool) -> Int32 -> f 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 -> f Int32) -> (Int32 -> Int32) -> Int32 -> f Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> Int32
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Int32 -> f Int32
previous = (Int32 -> Bool) -> Int32 -> f 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 -> f Int32) -> (Int32 -> Int32) -> Int32 -> f 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 -> f Int64
next = (Int64 -> Bool) -> Int64 -> f 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 -> f Int64) -> (Int64 -> Int64) -> Int64 -> f Int64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Int64
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Int64 -> f Int64
previous = (Int64 -> Bool) -> Int64 -> f 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 -> f Int64) -> (Int64 -> Int64) -> Int64 -> f 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 -> f Int
next = (Int -> Bool) -> Int -> f 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 -> f Int) -> (Int -> Int) -> Int -> f Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Int -> f Int
previous = (Int -> Bool) -> Int -> f 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 -> f Int) -> (Int -> Int) -> Int -> f 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 -> f Word
next = (Word -> Bool) -> Word -> f 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 -> f Word) -> (Word -> Word) -> Word -> f Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> Word
forall a. Num a => a -> a
inc
  {-# INLINE previous #-}
  previous :: Word -> f Word
previous = (Word -> Bool) -> Word -> f 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 -> f Word) -> (Word -> Word) -> Word -> f 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 -> f (Finite n)
next = (Finite n -> Bool) -> Finite n -> f (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 -> f (Finite n))
-> (Finite n -> Finite n) -> Finite n -> f (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 -> f (Finite n)
previous = (Finite n -> Bool) -> Finite n -> f (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 -> f (Finite n))
-> (Finite n -> Finite n) -> Finite n -> f (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
. Finite (Cardinality a) -> Finite (Cardinality a)
opp
    where 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
- 1)) (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
+ 1) (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 
          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
  {-# INLINE toFinite #-}
  toFinite :: Down a -> Finite (Cardinality (Down a))
toFinite = (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))
-> (Down a -> Natural) -> Down 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) -> (Down a -> Natural) -> Down 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
- 1)) (Natural -> Natural) -> (Down a -> Natural) -> Down a -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ 1) (Natural -> Natural) -> (Down a -> Natural) -> Down 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 (Finite (Cardinality a) -> Natural)
-> (Down a -> Finite (Cardinality a)) -> Down a -> Natural
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))
-> (Down a -> a) -> Down a -> Finite (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Down a) -> Down a -> a
forall a b (to :: Type -> Type -> Type).
Coercible a b =>
to a b -> b -> a
op a -> Down a
forall a. a -> Down a
Down
    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 

-- | 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 i :: 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 ix :: 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 i :: 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 ix :: 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 i :: 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 ix :: 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 x :: 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 (f :: Type -> Type).
(Finitary a, Alternative f) =>
a -> f 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 x :: 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
<$> [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 lo :: a
lo hi :: 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
. (\x :: 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
. (\x :: 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 v :: MVector v n (PrimState m) a
v acc :: 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)) 
                               (\Refl -> do let (d :: Finite (Cardinality a ^ (n - 1))
d, r :: 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 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 v :: 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
          Nothing -> 0
          Just Refl -> let (h :: a
h, t :: 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
+ 1)

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

{-# INLINE guarded #-}
guarded :: forall (a :: Type) (f :: Type -> Type) . (Alternative f) => (a -> Bool) -> a -> f a
guarded :: (a -> Bool) -> a -> f a
guarded p :: a -> Bool
p x :: 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)