{-# 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 #-}
module Data.Finite
(
Finite(..), cardinality, enumerate, asFin
, 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(..))
class Finite a where
type Cardinality a :: Nat
cardinality' :: SC a (Cardinality a)
toFin :: a -> Fin (Cardinality a)
fromFin :: Fin (Cardinality a) -> a
newtype SC a n = SC { SC a n -> SInt n
getSC :: SInt n }
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)
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)
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
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
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
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
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
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 #-}
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))