-- Copyright 2019-2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Provides a class of types isomorphic to some statically-known @'Fin' n@.
--
-- This comes with Generics-based generated instances, and can be used to
-- generate instances of 'Enum' and 'Bounded' (for which the stock deriving
-- only supports sum types with no fields).
--
-- Since this is all still represented by 'Int' internally, things will start
-- raising 'error's if your type has more values than can fit in positive
-- 'Int's.  It's not recommended to use this on large types, and there's not
-- much reason to want to anyway, as its main uses are to derive 'Enum' (which
-- is also based on 'Int') and to make the type compatible with
-- 'Data.Finite.Table.Table' (which would be impractically large for a key type
-- with too many values to represent as 'Int').
--
-- The most common way to get a 'Finite' instance for a type is to tack on a
-- @deriving Finite via 'Wrapped' 'Generic' MyType@ clause, which results in an
-- automatically-generated instance based on the type's ADT structure.
--
-- This also provides instances @'Enum' (Wrapped Finite a)@ and
-- @'Bounded' (Wrapped Finite a)@, so some types that would otherwise not be
-- compatible with derived 'Enum' instances can get them by adding a
-- @deriving (Enum, Bounded) via Wrapped Finite MyType@ clause.

module Data.Finite
         ( -- * Finite Enumerations
           Finite(..), cardinality, enumerate, asFin
           -- * Implementation Details
         , SC, GFinite(..), GCardinality
         ) where

import Data.Functor.Identity (Identity)
import Data.Int (Int8, Int16)
import Data.Proxy (Proxy(..))
import Data.Semigroup (WrappedMonoid, Min, Max, First, Last)
import Data.Void (Void)
import Data.Word (Word8, Word16)
import GHC.Generics
         ( Generic(..), V1, U1(..), M1(..), K1(..), (:+:)(..), (:*:)(..)
         )
import GHC.TypeNats (type (+), type (*), type (<=), KnownNat, Nat, natVal)

import Control.Lens (Iso', iso)
import Data.SInt (SInt, sintVal, addSInt, mulSInt, staticSIntVal, reifySInt)

import Data.Fin.Int.Explicit
         ( enumFin, concatFin, splitFin, crossFin, divModFin, minFin, maxFin
         , fin
         )
import Data.Fin.Int (Fin, finToInt, unsafeFin)
import qualified Data.Vec.Short as V
import Data.Wrapped (Wrapped(..))

-- | A typeclass of finite enumerable types.
--
-- These allow constructing 'Data.Functor.Rep.Representable' Functors using a
-- simple 'Data.Vec.Short.Vec' as the underlying storage, with constant-time
-- lookup and efficient traversals.
--
-- Note that since 'Fin' is (currently) represented by 'Int', any type with
-- more values than 'Int' can't have an instance.  This means we can't have
-- instances for 32- and 64-bit arithmetic types, since 'Int' is only required
-- to have 30 bits of precision.
--
-- Annoyingly, we also can't have an instance for 'Int' and 'Word', because
-- 'Fin' wastes one bit of the 'Int' by forbidding negative values.  The
-- cardinality of 'Int' and 'Word' would need to be twice as large as we can
-- actually represent in a 'Fin'.  Another obstacle is that their cardinality
-- varies between implementations and architectures; it's possible to work
-- around this by making their Cardinality an irreducible type family
-- application, and using 'Data.SInt.SI#' to plug in a value at runtime, but
-- this makes the 'Fin's related to 'Int' and 'Word' annoying to work with,
-- since their bound is only known at runtime.
--
-- Fortunately, those instances are unlikely to be important, since a table of
-- 2^32 elements is moderately impractical (32GiB of pointers alone), and a
-- table of 2^64 elements is unrepresentable in current computer architectures.
--
-- 'toFin' and 'fromFin' shall be total functions and shall be the two sides of
-- an isomorphism.
class Finite a where
  type Cardinality a :: Nat
  -- | A witness that the cardinality is known at runtime.
  --
  -- This isn't part of the class context because we can only perform
  -- arithmetic on 'KnownNat' instances in expression context; that is, we
  -- can't convince GHC that an instance with
  -- @type Cardinality (Maybe a) = Cardinality a + 1@ is valid if the
  -- 'KnownNat' is in the class context.  Instead, we use 'SInt' to allow
  -- computing the cardinality at runtime.
  cardinality' :: SC a (Cardinality a)

  toFin :: a -> Fin (Cardinality a)
  fromFin :: Fin (Cardinality a) -> a

-- | A wrapper type around @'Cardinality' a@ to support DerivingVia on GHC 8.6.
--
-- Instance methods that don't mention the instance head outside of type
-- families / aliases don't work with DerivingVia on GHC 8.6 because it uses
-- type signatures rather than TypeApplications to choose the instance to call
-- into.
newtype SC a n = SC { SC a n -> SInt n
getSC :: SInt n }

-- | A witness that the cardinality of @a@ is known at runtime.
cardinality :: forall a. Finite a => SInt (Cardinality a)
cardinality :: SInt (Cardinality a)
cardinality = SC a (Cardinality a) -> SInt (Cardinality a)
forall k (a :: k) (n :: Nat). SC a n -> SInt n
getSC (Finite a => SC a (Cardinality a)
forall a. Finite a => SC a (Cardinality a)
cardinality' @a)

-- | Generate a list containing every value of @a@.
enumerate :: forall a. Finite a => [a]
enumerate :: [a]
enumerate = Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin (Fin (Cardinality a) -> a) -> [Fin (Cardinality a)] -> [a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SInt (Cardinality a) -> [Fin (Cardinality a)]
forall (n :: Nat). SInt n -> [Fin n]
enumFin (Finite a => SInt (Cardinality a)
forall a. Finite a => SInt (Cardinality a)
cardinality @a)

-- | Implement 'toFin' by 'fromEnum'.
--
-- This should only be used for types with 'fromEnum' range @0..Cardinality a@;
-- this is notably not the case for signed integer types, which have negative
-- 'fromEnum' values.
toFinEnum :: Enum a => SInt (Cardinality a) -> a -> Fin (Cardinality a)
toFinEnum :: SInt (Cardinality a) -> a -> Fin (Cardinality a)
toFinEnum SInt (Cardinality a)
sn = SInt (Cardinality a) -> Int -> Fin (Cardinality a)
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin SInt (Cardinality a)
sn (Int -> Fin (Cardinality a))
-> (a -> Int) -> a -> Fin (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a. Enum a => a -> Int
fromEnum

-- | Implement 'fromFin' by 'toEnum'.
--
-- The same restrictions apply as for 'toFinEnum'.
fromFinEnum :: Enum a => Fin (Cardinality a) -> a
fromFinEnum :: Fin (Cardinality a) -> a
fromFinEnum = Int -> a
forall a. Enum a => Int -> a
toEnum (Int -> a)
-> (Fin (Cardinality a) -> Int) -> Fin (Cardinality a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> Int
forall (n :: Nat). Fin n -> Int
finToInt

instance Finite Char where
  type Cardinality Char = 1114112 -- According to 'minBound' and 'maxBound'
  cardinality' :: SC Char (Cardinality Char)
cardinality' = SInt 1114112 -> SC Char 1114112
forall k (a :: k) (n :: Nat). SInt n -> SC a n
SC SInt 1114112
forall (n :: Nat). (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n
staticSIntVal
  toFin :: Char -> Fin (Cardinality Char)
toFin = SInt (Cardinality Char) -> Char -> Fin (Cardinality Char)
forall a.
Enum a =>
SInt (Cardinality a) -> a -> Fin (Cardinality a)
toFinEnum SInt (Cardinality Char)
forall (n :: Nat). (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n
staticSIntVal
  fromFin :: Fin (Cardinality Char) -> Char
fromFin = Fin (Cardinality Char) -> Char
forall a. Enum a => Fin (Cardinality a) -> a
fromFinEnum

toFinExcessK
  :: forall n a. (KnownNat n, Integral a) => a -> Fin (Cardinality a)
toFinExcessK :: a -> Fin (Cardinality a)
toFinExcessK =
  Int -> Fin (Cardinality a)
forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin (Int -> Fin (Cardinality a))
-> (a -> Int) -> a -> Fin (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal @n Proxy n
forall k (t :: k). Proxy t
Proxy) :: Int)) (Int -> Int) -> (a -> Int) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral

fromFinExcessK
  :: forall n a. (KnownNat n, Integral a) => Fin (Cardinality a) -> a
fromFinExcessK :: Fin (Cardinality a) -> a
fromFinExcessK =
  a -> a -> a
forall a. Num a => a -> a -> a
subtract (Natural -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal @n Proxy n
forall k (t :: k). Proxy t
Proxy)) (a -> a) -> (Fin (Cardinality a) -> a) -> Fin (Cardinality a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> a)
-> (Fin (Cardinality a) -> Int) -> Fin (Cardinality a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> Int
forall (n :: Nat). Fin n -> Int
finToInt

instance Finite Int8 where
  type Cardinality Int8 = 256
  cardinality' :: SC Int8 (Cardinality Int8)
cardinality' = SInt 256 -> SC Int8 256
forall k (a :: k) (n :: Nat). SInt n -> SC a n
SC SInt 256
forall (n :: Nat). (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n
staticSIntVal
  toFin :: Int8 -> Fin (Cardinality Int8)
toFin = forall a. (KnownNat 128, Integral a) => a -> Fin (Cardinality a)
forall (n :: Nat) a.
(KnownNat n, Integral a) =>
a -> Fin (Cardinality a)
toFinExcessK @128
  fromFin :: Fin (Cardinality Int8) -> Int8
fromFin = forall a. (KnownNat 128, Integral a) => Fin (Cardinality a) -> a
forall (n :: Nat) a.
(KnownNat n, Integral a) =>
Fin (Cardinality a) -> a
fromFinExcessK @128

instance Finite Int16 where
  type Cardinality Int16 = 65536
  cardinality' :: SC Int16 (Cardinality Int16)
cardinality' = SInt 65536 -> SC Int16 65536
forall k (a :: k) (n :: Nat). SInt n -> SC a n
SC SInt 65536
forall (n :: Nat). (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n
staticSIntVal
  toFin :: Int16 -> Fin (Cardinality Int16)
toFin = forall a. (KnownNat 32768, Integral a) => a -> Fin (Cardinality a)
forall (n :: Nat) a.
(KnownNat n, Integral a) =>
a -> Fin (Cardinality a)
toFinExcessK @32768
  fromFin :: Fin (Cardinality Int16) -> Int16
fromFin = forall a. (KnownNat 32768, Integral a) => Fin (Cardinality a) -> a
forall (n :: Nat) a.
(KnownNat n, Integral a) =>
Fin (Cardinality a) -> a
fromFinExcessK @32768

instance Finite Word8 where
  type Cardinality Word8 = 256
  cardinality' :: SC Word8 (Cardinality Word8)
cardinality' = SInt 256 -> SC Word8 256
forall k (a :: k) (n :: Nat). SInt n -> SC a n
SC SInt 256
forall (n :: Nat). (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n
staticSIntVal
  toFin :: Word8 -> Fin (Cardinality Word8)
toFin = Int -> Fin 256
forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin (Int -> Fin 256) -> (Word8 -> Int) -> Word8 -> Fin 256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. a -> a
id @Int (Int -> Int) -> (Word8 -> Int) -> Word8 -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  fromFin :: Fin (Cardinality Word8) -> Word8
fromFin = Int -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word8) -> (Fin 256 -> Int) -> Fin 256 -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin 256 -> Int
forall (n :: Nat). Fin n -> Int
finToInt

instance Finite Word16 where
  type Cardinality Word16 = 65536
  cardinality' :: SC Word16 (Cardinality Word16)
cardinality' = SInt 65536 -> SC Word16 65536
forall k (a :: k) (n :: Nat). SInt n -> SC a n
SC SInt 65536
forall (n :: Nat). (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n
staticSIntVal
  toFin :: Word16 -> Fin (Cardinality Word16)
toFin = Int -> Fin 65536
forall a (n :: Nat). Integral a => a -> Fin n
unsafeFin (Int -> Fin 65536) -> (Word16 -> Int) -> Word16 -> Fin 65536
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. a -> a
id @Int (Int -> Int) -> (Word16 -> Int) -> Word16 -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word16 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  fromFin :: Fin (Cardinality Word16) -> Word16
fromFin = Int -> Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word16) -> (Fin 65536 -> Int) -> Fin 65536 -> Word16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin 65536 -> Int
forall (n :: Nat). Fin n -> Int
finToInt

instance KnownNat n => Finite (Fin n) where
  type Cardinality (Fin n) = n
  cardinality' :: SC (Fin n) (Cardinality (Fin n))
cardinality' = SInt n -> SC (Fin n) n
forall k (a :: k) (n :: Nat). SInt n -> SC a n
SC SInt n
forall (n :: Nat). (HasCallStack, KnownNat n) => SInt n
sintVal
  toFin :: Fin n -> Fin (Cardinality (Fin n))
toFin = Fin n -> Fin (Cardinality (Fin n))
forall a. a -> a
id
  fromFin :: Fin (Cardinality (Fin n)) -> Fin n
fromFin = Fin (Cardinality (Fin n)) -> Fin n
forall a. a -> a
id

-- Aesthetics: make more derived instances fit on one line.
type G = Wrapped Generic

deriving via G () instance Finite ()
deriving via G Bool instance Finite Bool
deriving via G Ordering instance Finite Ordering
deriving via G Void instance Finite Void
deriving via G (Identity a) instance Finite a => Finite (Identity a)
deriving via G (WrappedMonoid a) instance Finite a => Finite (WrappedMonoid a)
deriving via G (Last a) instance Finite a => Finite (Last a)
deriving via G (First a) instance Finite a => Finite (First a)
deriving via G (Max a) instance Finite a => Finite (Max a)
deriving via G (Min a) instance Finite a => Finite (Min a)
deriving via G (Maybe a) instance Finite a => Finite (Maybe a)
deriving via G (Either a b) instance (Finite a, Finite b) => Finite (Either a b)

deriving via G (a, b) instance (Finite a, Finite b) => Finite (a, b)
deriving via G (a, b, c)
  instance (Finite a, Finite b, Finite c) => Finite (a, b, c)

deriving via G (a, b, c, d)
  instance (Finite a, Finite b, Finite c, Finite d) => Finite (a, b, c, d)
deriving via G (a, b, c, d, e)
  instance (Finite a, Finite b, Finite c, Finite d, Finite e)
        => Finite (a, b, c, d, e)

instance (Generic a, GFinite (Rep a)) => Finite (Wrapped Generic a) where
  type Cardinality (Wrapped Generic a) = GCardinality (Rep a)
  cardinality' :: SC (Wrapped Generic a) (Cardinality (Wrapped Generic a))
cardinality' = SInt (GCardinality (Rep a))
-> SC (Wrapped Generic a) (GCardinality (Rep a))
forall k (a :: k) (n :: Nat). SInt n -> SC a n
SC (SInt (GCardinality (Rep a))
 -> SC (Wrapped Generic a) (GCardinality (Rep a)))
-> SInt (GCardinality (Rep a))
-> SC (Wrapped Generic a) (GCardinality (Rep a))
forall a b. (a -> b) -> a -> b
$ GFinite (Rep a) => SInt (GCardinality (Rep a))
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @(Rep a)
  toFin :: Wrapped Generic a -> Fin (Cardinality (Wrapped Generic a))
toFin = Rep a Any -> Fin (GCardinality (Rep a))
forall k (a :: k -> Type) (p :: k).
GFinite a =>
a p -> Fin (GCardinality a)
gtoFin (Rep a Any -> Fin (GCardinality (Rep a)))
-> (Wrapped Generic a -> Rep a Any)
-> Wrapped Generic a
-> Fin (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 (a -> Rep a Any)
-> (Wrapped Generic a -> a) -> Wrapped Generic a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapped Generic a -> a
forall (c :: Type -> Constraint) a. Wrapped c a -> a
unWrapped
  fromFin :: Fin (Cardinality (Wrapped Generic a)) -> Wrapped Generic a
fromFin = a -> Wrapped Generic a
forall (c :: Type -> Constraint) a. a -> Wrapped c a
Wrapped (a -> Wrapped Generic a)
-> (Fin (GCardinality (Rep a)) -> a)
-> Fin (GCardinality (Rep a))
-> Wrapped Generic a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (Rep a Any -> a)
-> (Fin (GCardinality (Rep a)) -> Rep a Any)
-> Fin (GCardinality (Rep a))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (GCardinality (Rep a)) -> Rep a Any
forall k (a :: k -> Type) (p :: k).
GFinite a =>
Fin (GCardinality a) -> a p
gfromFin

-- | The derived cardinality of a generic representation type.
type family GCardinality a where
  GCardinality V1         = 0
  GCardinality U1         = 1
  GCardinality (K1 i a)   = Cardinality a
  GCardinality (M1 i c f) = GCardinality f
  GCardinality (f :+: g)  = GCardinality f + GCardinality g
  GCardinality (f :*: g)  = GCardinality f * GCardinality g

-- | The derived 'Finite' implementation of a generic representation type.
class GFinite a where
  gcardinality :: SInt (GCardinality a)
  gtoFin :: a p -> Fin (GCardinality a)
  gfromFin :: Fin (GCardinality a) -> a p

instance GFinite V1 where
  gcardinality :: SInt (GCardinality V1)
gcardinality = SInt (GCardinality V1)
forall (n :: Nat). (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n
staticSIntVal
  gtoFin :: V1 p -> Fin (GCardinality V1)
gtoFin V1 p
x = case V1 p
x of {}
  gfromFin :: Fin (GCardinality V1) -> V1 p
gfromFin Fin (GCardinality V1)
x = Vec 0 (V1 p)
forall a. Vec 0 a
V.nil Vec 0 (V1 p) -> Fin 0 -> V1 p
forall (n :: Nat) a. Vec n a -> Fin n -> a
V.! Fin 0
Fin (GCardinality V1)
x

instance GFinite U1 where
  gcardinality :: SInt (GCardinality U1)
gcardinality = SInt (GCardinality U1)
forall (n :: Nat). (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n
staticSIntVal
  gtoFin :: U1 p -> Fin (GCardinality U1)
gtoFin U1 p
U1 = Fin (GCardinality U1)
forall (n :: Nat). (1 <= n) => Fin n
minFin
  gfromFin :: Fin (GCardinality U1) -> U1 p
gfromFin !Fin (GCardinality U1)
_ = U1 p
forall k (p :: k). U1 p
U1

instance Finite a => GFinite (K1 i a) where
  gcardinality :: SInt (GCardinality (K1 i a))
gcardinality = Finite a => SInt (Cardinality a)
forall a. Finite a => SInt (Cardinality a)
cardinality @a
  gtoFin :: K1 i a p -> Fin (GCardinality (K1 i a))
gtoFin = a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin (a -> Fin (Cardinality a))
-> (K1 i a p -> a) -> K1 i a p -> Fin (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i a p -> a
forall i c k (p :: k). K1 i c p -> c
unK1
  gfromFin :: Fin (GCardinality (K1 i a)) -> K1 i a p
gfromFin = a -> K1 i a p
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a p)
-> (Fin (Cardinality a) -> a) -> Fin (Cardinality a) -> K1 i a p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin

instance GFinite f => GFinite (M1 i c f) where
  gcardinality :: SInt (GCardinality (M1 i c f))
gcardinality = GFinite f => SInt (GCardinality f)
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @f
  gtoFin :: M1 i c f p -> Fin (GCardinality (M1 i c f))
gtoFin = f p -> Fin (GCardinality f)
forall k (a :: k -> Type) (p :: k).
GFinite a =>
a p -> Fin (GCardinality a)
gtoFin (f p -> Fin (GCardinality f))
-> (M1 i c f p -> f p) -> M1 i c f p -> Fin (GCardinality f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f p -> f p
forall i (c :: Meta) k (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1
  gfromFin :: Fin (GCardinality (M1 i c f)) -> M1 i c f p
gfromFin = f p -> M1 i c f p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (f p -> M1 i c f p)
-> (Fin (GCardinality f) -> f p)
-> Fin (GCardinality f)
-> M1 i c f p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (GCardinality f) -> f p
forall k (a :: k -> Type) (p :: k).
GFinite a =>
Fin (GCardinality a) -> a p
gfromFin

instance (GFinite f, GFinite g) => GFinite (f :+: g) where
  gcardinality :: SInt (GCardinality (f :+: g))
gcardinality = GFinite f => SInt (GCardinality f)
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @f SInt (GCardinality f)
-> SInt (GCardinality g) -> SInt (GCardinality f + GCardinality g)
forall (m :: Nat) (n :: Nat).
HasCallStack =>
SInt m -> SInt n -> SInt (m + n)
`addSInt` GFinite g => SInt (GCardinality g)
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @g
  gtoFin :: (:+:) f g p -> Fin (GCardinality (f :+: g))
gtoFin (:+:) f g p
x = SInt (GCardinality f)
-> Either (Fin (GCardinality f)) (Fin (GCardinality g))
-> Fin (GCardinality f + GCardinality g)
forall (m :: Nat) (n :: Nat).
SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)
concatFin (GFinite f => SInt (GCardinality f)
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @f) (Either (Fin (GCardinality f)) (Fin (GCardinality g))
 -> Fin (GCardinality f + GCardinality g))
-> Either (Fin (GCardinality f)) (Fin (GCardinality g))
-> Fin (GCardinality f + GCardinality g)
forall a b. (a -> b) -> a -> b
$ case (:+:) f g p
x of
    L1 f p
f -> Fin (GCardinality f)
-> Either (Fin (GCardinality f)) (Fin (GCardinality g))
forall a b. a -> Either a b
Left (Fin (GCardinality f)
 -> Either (Fin (GCardinality f)) (Fin (GCardinality g)))
-> Fin (GCardinality f)
-> Either (Fin (GCardinality f)) (Fin (GCardinality g))
forall a b. (a -> b) -> a -> b
$ f p -> Fin (GCardinality f)
forall k (a :: k -> Type) (p :: k).
GFinite a =>
a p -> Fin (GCardinality a)
gtoFin f p
f
    R1 g p
g -> Fin (GCardinality g)
-> Either (Fin (GCardinality f)) (Fin (GCardinality g))
forall a b. b -> Either a b
Right (Fin (GCardinality g)
 -> Either (Fin (GCardinality f)) (Fin (GCardinality g)))
-> Fin (GCardinality g)
-> Either (Fin (GCardinality f)) (Fin (GCardinality g))
forall a b. (a -> b) -> a -> b
$ g p -> Fin (GCardinality g)
forall k (a :: k -> Type) (p :: k).
GFinite a =>
a p -> Fin (GCardinality a)
gtoFin g p
g
  gfromFin :: Fin (GCardinality (f :+: g)) -> (:+:) f g p
gfromFin =
    (Fin (GCardinality f) -> (:+:) f g p)
-> (Fin (GCardinality g) -> (:+:) f g p)
-> Either (Fin (GCardinality f)) (Fin (GCardinality g))
-> (:+:) f g p
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (f p -> (:+:) f g p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (f p -> (:+:) f g p)
-> (Fin (GCardinality f) -> f p)
-> Fin (GCardinality f)
-> (:+:) f g p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (GCardinality f) -> f p
forall k (a :: k -> Type) (p :: k).
GFinite a =>
Fin (GCardinality a) -> a p
gfromFin) (g p -> (:+:) f g p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (g p -> (:+:) f g p)
-> (Fin (GCardinality g) -> g p)
-> Fin (GCardinality g)
-> (:+:) f g p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (GCardinality g) -> g p
forall k (a :: k -> Type) (p :: k).
GFinite a =>
Fin (GCardinality a) -> a p
gfromFin) (Either (Fin (GCardinality f)) (Fin (GCardinality g))
 -> (:+:) f g p)
-> (Fin (GCardinality f + GCardinality g)
    -> Either (Fin (GCardinality f)) (Fin (GCardinality g)))
-> Fin (GCardinality f + GCardinality g)
-> (:+:) f g p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInt (GCardinality f)
-> Fin (GCardinality f + GCardinality g)
-> Either (Fin (GCardinality f)) (Fin (GCardinality g))
forall (m :: Nat) (n :: Nat).
SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
splitFin (GFinite f => SInt (GCardinality f)
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @f)
  {-# INLINE gtoFin #-}
  {-# INLINE gfromFin #-}

instance (GFinite f, GFinite g) => GFinite (f :*: g) where
  gcardinality :: SInt (GCardinality (f :*: g))
gcardinality = GFinite f => SInt (GCardinality f)
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @f SInt (GCardinality f)
-> SInt (GCardinality g) -> SInt (GCardinality f * GCardinality g)
forall (m :: Nat) (n :: Nat).
HasCallStack =>
SInt m -> SInt n -> SInt (m * n)
`mulSInt` GFinite g => SInt (GCardinality g)
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @g
  gtoFin :: (:*:) f g p -> Fin (GCardinality (f :*: g))
gtoFin (f p
f :*: g p
g) = SInt (GCardinality g)
-> Fin (GCardinality f)
-> Fin (GCardinality g)
-> Fin (GCardinality f * GCardinality g)
forall (n :: Nat) (m :: Nat).
SInt n -> Fin m -> Fin n -> Fin (m * n)
crossFin (GFinite g => SInt (GCardinality g)
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @g) (f p -> Fin (GCardinality f)
forall k (a :: k -> Type) (p :: k).
GFinite a =>
a p -> Fin (GCardinality a)
gtoFin f p
f) (g p -> Fin (GCardinality g)
forall k (a :: k -> Type) (p :: k).
GFinite a =>
a p -> Fin (GCardinality a)
gtoFin g p
g)
  gfromFin :: Fin (GCardinality (f :*: g)) -> (:*:) f g p
gfromFin Fin (GCardinality (f :*: g))
x =
    let (Fin (GCardinality f)
f, Fin (GCardinality g)
g) = SInt (GCardinality g)
-> Fin (GCardinality f * GCardinality g)
-> (Fin (GCardinality f), Fin (GCardinality g))
forall (m :: Nat) (d :: Nat).
SInt m -> Fin (d * m) -> (Fin d, Fin m)
divModFin (GFinite g => SInt (GCardinality g)
forall k (a :: k -> Type). GFinite a => SInt (GCardinality a)
gcardinality @g) Fin (GCardinality f * GCardinality g)
Fin (GCardinality (f :*: g))
x
    in  Fin (GCardinality f) -> f p
forall k (a :: k -> Type) (p :: k).
GFinite a =>
Fin (GCardinality a) -> a p
gfromFin Fin (GCardinality f)
f f p -> g p -> (:*:) f g p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: Fin (GCardinality g) -> g p
forall k (a :: k -> Type) (p :: k).
GFinite a =>
Fin (GCardinality a) -> a p
gfromFin Fin (GCardinality g)
g
  {-# INLINE gtoFin #-}
  {-# INLINE gfromFin #-}

-- | An 'Control.Lens.Iso' between @a@ and the corresponding 'Fin' type.
asFin :: Finite a => Iso' a (Fin (Cardinality a))
asFin :: Iso' a (Fin (Cardinality a))
asFin = (a -> Fin (Cardinality a))
-> (Fin (Cardinality a) -> a) -> Iso' a (Fin (Cardinality a))
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin

instance Finite a => Enum (Wrapped Finite a) where
  toEnum :: Int -> Wrapped Finite a
toEnum = a -> Wrapped Finite a
forall (c :: Type -> Constraint) a. a -> Wrapped c a
Wrapped (a -> Wrapped Finite a) -> (Int -> a) -> Int -> Wrapped Finite a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin (Fin (Cardinality a) -> a)
-> (Int -> Fin (Cardinality a)) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInt (Cardinality a) -> Int -> Fin (Cardinality a)
forall (n :: Nat). HasCallStack => SInt n -> Int -> Fin n
fin (Finite a => SInt (Cardinality a)
forall a. Finite a => SInt (Cardinality a)
cardinality @a)
  fromEnum :: Wrapped Finite a -> Int
fromEnum = Fin (Cardinality a) -> Int
forall (n :: Nat). Fin n -> Int
finToInt (Fin (Cardinality a) -> Int)
-> (Wrapped Finite a -> Fin (Cardinality a))
-> Wrapped Finite a
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin (a -> Fin (Cardinality a))
-> (Wrapped Finite a -> a)
-> Wrapped Finite a
-> Fin (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapped Finite a -> a
forall (c :: Type -> Constraint) a. Wrapped c a -> a
unWrapped
  enumFrom :: Wrapped Finite a -> [Wrapped Finite a]
enumFrom = SInt (Cardinality a)
-> (KnownNat (Cardinality a) =>
    Wrapped Finite a -> [Wrapped Finite a])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall (n :: Nat) r. SInt n -> (KnownNat n => r) -> r
reifySInt (Finite a => SInt (Cardinality a)
forall a. Finite a => SInt (Cardinality a)
cardinality @a) ((KnownNat (Cardinality a) =>
  Wrapped Finite a -> [Wrapped Finite a])
 -> Wrapped Finite a -> [Wrapped Finite a])
-> (KnownNat (Cardinality a) =>
    Wrapped Finite a -> [Wrapped Finite a])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall a b. (a -> b) -> a -> b
$
    (Fin (Cardinality a) -> Wrapped Finite a)
-> [Fin (Cardinality a)] -> [Wrapped Finite a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> Wrapped Finite a
forall (c :: Type -> Constraint) a. a -> Wrapped c a
Wrapped (a -> Wrapped Finite a)
-> (Fin (Cardinality a) -> a)
-> Fin (Cardinality a)
-> Wrapped Finite a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin) ([Fin (Cardinality a)] -> [Wrapped Finite a])
-> (Wrapped Finite a -> [Fin (Cardinality a)])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> [Fin (Cardinality a)]
forall a. Enum a => a -> [a]
enumFrom (Fin (Cardinality a) -> [Fin (Cardinality a)])
-> (Wrapped Finite a -> Fin (Cardinality a))
-> Wrapped Finite a
-> [Fin (Cardinality a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin (a -> Fin (Cardinality a))
-> (Wrapped Finite a -> a)
-> Wrapped Finite a
-> Fin (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapped Finite a -> a
forall (c :: Type -> Constraint) a. Wrapped c a -> a
unWrapped
  enumFromThen :: Wrapped Finite a -> Wrapped Finite a -> [Wrapped Finite a]
enumFromThen (Wrapped a
x) = SInt (Cardinality a)
-> (KnownNat (Cardinality a) =>
    Wrapped Finite a -> [Wrapped Finite a])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall (n :: Nat) r. SInt n -> (KnownNat n => r) -> r
reifySInt (Finite a => SInt (Cardinality a)
forall a. Finite a => SInt (Cardinality a)
cardinality @a) ((KnownNat (Cardinality a) =>
  Wrapped Finite a -> [Wrapped Finite a])
 -> Wrapped Finite a -> [Wrapped Finite a])
-> (KnownNat (Cardinality a) =>
    Wrapped Finite a -> [Wrapped Finite a])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall a b. (a -> b) -> a -> b
$
    (Fin (Cardinality a) -> Wrapped Finite a)
-> [Fin (Cardinality a)] -> [Wrapped Finite a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> Wrapped Finite a
forall (c :: Type -> Constraint) a. a -> Wrapped c a
Wrapped (a -> Wrapped Finite a)
-> (Fin (Cardinality a) -> a)
-> Fin (Cardinality a)
-> Wrapped Finite a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin) ([Fin (Cardinality a)] -> [Wrapped Finite a])
-> (Wrapped Finite a -> [Fin (Cardinality a)])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> Fin (Cardinality a) -> [Fin (Cardinality a)]
forall a. Enum a => a -> a -> [a]
enumFromThen (a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin a
x) (Fin (Cardinality a) -> [Fin (Cardinality a)])
-> (Wrapped Finite a -> Fin (Cardinality a))
-> Wrapped Finite a
-> [Fin (Cardinality a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin (a -> Fin (Cardinality a))
-> (Wrapped Finite a -> a)
-> Wrapped Finite a
-> Fin (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapped Finite a -> a
forall (c :: Type -> Constraint) a. Wrapped c a -> a
unWrapped
  enumFromTo :: Wrapped Finite a -> Wrapped Finite a -> [Wrapped Finite a]
enumFromTo (Wrapped a
x) = SInt (Cardinality a)
-> (KnownNat (Cardinality a) =>
    Wrapped Finite a -> [Wrapped Finite a])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall (n :: Nat) r. SInt n -> (KnownNat n => r) -> r
reifySInt (Finite a => SInt (Cardinality a)
forall a. Finite a => SInt (Cardinality a)
cardinality @a) ((KnownNat (Cardinality a) =>
  Wrapped Finite a -> [Wrapped Finite a])
 -> Wrapped Finite a -> [Wrapped Finite a])
-> (KnownNat (Cardinality a) =>
    Wrapped Finite a -> [Wrapped Finite a])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall a b. (a -> b) -> a -> b
$
    (Fin (Cardinality a) -> Wrapped Finite a)
-> [Fin (Cardinality a)] -> [Wrapped Finite a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> Wrapped Finite a
forall (c :: Type -> Constraint) a. a -> Wrapped c a
Wrapped (a -> Wrapped Finite a)
-> (Fin (Cardinality a) -> a)
-> Fin (Cardinality a)
-> Wrapped Finite a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin) ([Fin (Cardinality a)] -> [Wrapped Finite a])
-> (Wrapped Finite a -> [Fin (Cardinality a)])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> Fin (Cardinality a) -> [Fin (Cardinality a)]
forall a. Enum a => a -> a -> [a]
enumFromTo (a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin a
x) (Fin (Cardinality a) -> [Fin (Cardinality a)])
-> (Wrapped Finite a -> Fin (Cardinality a))
-> Wrapped Finite a
-> [Fin (Cardinality a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin (a -> Fin (Cardinality a))
-> (Wrapped Finite a -> a)
-> Wrapped Finite a
-> Fin (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapped Finite a -> a
forall (c :: Type -> Constraint) a. Wrapped c a -> a
unWrapped
  enumFromThenTo :: Wrapped Finite a
-> Wrapped Finite a -> Wrapped Finite a -> [Wrapped Finite a]
enumFromThenTo (Wrapped a
x) (Wrapped a
y) = SInt (Cardinality a)
-> (KnownNat (Cardinality a) =>
    Wrapped Finite a -> [Wrapped Finite a])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall (n :: Nat) r. SInt n -> (KnownNat n => r) -> r
reifySInt (Finite a => SInt (Cardinality a)
forall a. Finite a => SInt (Cardinality a)
cardinality @a) ((KnownNat (Cardinality a) =>
  Wrapped Finite a -> [Wrapped Finite a])
 -> Wrapped Finite a -> [Wrapped Finite a])
-> (KnownNat (Cardinality a) =>
    Wrapped Finite a -> [Wrapped Finite a])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall a b. (a -> b) -> a -> b
$
    (Fin (Cardinality a) -> Wrapped Finite a)
-> [Fin (Cardinality a)] -> [Wrapped Finite a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> Wrapped Finite a
forall (c :: Type -> Constraint) a. a -> Wrapped c a
Wrapped (a -> Wrapped Finite a)
-> (Fin (Cardinality a) -> a)
-> Fin (Cardinality a)
-> Wrapped Finite a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin) ([Fin (Cardinality a)] -> [Wrapped Finite a])
-> (Wrapped Finite a -> [Fin (Cardinality a)])
-> Wrapped Finite a
-> [Wrapped Finite a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (Cardinality a)
-> Fin (Cardinality a)
-> Fin (Cardinality a)
-> [Fin (Cardinality a)]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo (a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin a
x) (a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin a
y) (Fin (Cardinality a) -> [Fin (Cardinality a)])
-> (Wrapped Finite a -> Fin (Cardinality a))
-> Wrapped Finite a
-> [Fin (Cardinality a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    a -> Fin (Cardinality a)
forall a. Finite a => a -> Fin (Cardinality a)
toFin (a -> Fin (Cardinality a))
-> (Wrapped Finite a -> a)
-> Wrapped Finite a
-> Fin (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrapped Finite a -> a
forall (c :: Type -> Constraint) a. Wrapped c a -> a
unWrapped

instance (Finite a, 1 <= Cardinality a) => Bounded (Wrapped Finite a) where
  minBound :: Wrapped Finite a
minBound = a -> Wrapped Finite a
forall (c :: Type -> Constraint) a. a -> Wrapped c a
Wrapped (a -> Wrapped Finite a) -> a -> Wrapped Finite a
forall a b. (a -> b) -> a -> b
$ Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin Fin (Cardinality a)
forall (n :: Nat). (1 <= n) => Fin n
minFin
  maxBound :: Wrapped Finite a
maxBound = a -> Wrapped Finite a
forall (c :: Type -> Constraint) a. a -> Wrapped c a
Wrapped (a -> Wrapped Finite a) -> a -> Wrapped Finite a
forall a b. (a -> b) -> a -> b
$ Fin (Cardinality a) -> a
forall a. Finite a => Fin (Cardinality a) -> a
fromFin (SInt (Cardinality a) -> Fin (Cardinality a)
forall (n :: Nat). (1 <= n) => SInt n -> Fin n
maxFin (Finite a => SInt (Cardinality a)
forall a. Finite a => SInt (Cardinality a)
cardinality @a))