{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DefaultSignatures #-}
module Data.Finitary.Enum(
  Enum(..),
  describeEnum,
  eqDefault,
  compareDefault,
  enumList,
  enum,
  coenum,
  cardinality,
  ptraverseFunction,
) where

import Data.Void

import Control.Applicative
import Data.Bifunctor.Clown

import Data.Profunctor.Cartesian

import Data.Word
import Data.Int

import Data.Functor.Contravariant.Divisible
import GHC.TypeNats (KnownNat (..), natVal)
import Data.Finite (Finite, shift, unshift, finites)
import Data.Finitary (Finitary(..))
import Prelude hiding (Enum)
import Data.Profunctor.FinFn
import Data.Functor.Contravariant (Contravariant(..))
import Data.Profunctor (Profunctor(..))

-- | @Enum x@ is @Finitary x@ but you can't get @Cardinality n@ at type level.
class (Ord x) => Enum x where
  enumeration :: FinFn x x
  enumeration = (forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> FinFn x x)
-> FinFn x x
forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
forall r.
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum (x -> Finite n) -> (Finite n -> x) -> FinFn x x
forall (n :: Nat).
KnownNat n =>
(x -> Finite n) -> (Finite n -> x) -> FinFn x x
forall (n :: Nat) a b.
KnownNat n =>
(a -> Finite n) -> (Finite n -> b) -> FinFn a b
makeFinFn

  withEnum :: (forall n. KnownNat n => (x -> Finite n) -> (Finite n -> x) -> r) -> r
  default withEnum :: Finitary x => (forall n. KnownNat n => (x -> Finite n) -> (Finite n -> x) -> r) -> r
  withEnum forall (n :: Nat).
KnownNat n =>
(x -> Finite n) -> (Finite n -> x) -> r
k = (x -> Finite (Cardinality x)) -> (Finite (Cardinality x) -> x) -> r
forall (n :: Nat).
KnownNat n =>
(x -> Finite n) -> (Finite n -> x) -> r
k x -> Finite (Cardinality x)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite Finite (Cardinality x) -> x
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite

eqDefault :: forall x. Enum x => x -> x -> Bool
eqDefault :: forall x. Enum x => x -> x -> Bool
eqDefault x
x1 x
x2 = (forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> Bool)
-> Bool
forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
forall r.
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum (\x -> Finite n
toF Finite n -> x
_ -> x -> Finite n
toF x
x1 Finite n -> Finite n -> Bool
forall a. Eq a => a -> a -> Bool
== x -> Finite n
toF x
x2)

compareDefault :: forall x. Enum x => x -> x -> Ordering
compareDefault :: forall x. Enum x => x -> x -> Ordering
compareDefault x
x1 x
x2 = (forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> Ordering)
-> Ordering
forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
forall r.
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum (\x -> Finite n
toF Finite n -> x
_ -> Finite n -> Finite n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (x -> Finite n
toF x
x1) (x -> Finite n
toF x
x2))

enum :: (Enum x, Alternative f) => f x
enum :: forall x (f :: * -> *). (Enum x, Alternative f) => f x
enum = (forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> f x)
-> f x
forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
forall r.
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum (\x -> Finite n
_ Finite n -> x
from -> [f x] -> f x
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum (x -> f x
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (x -> f x) -> (Finite n -> x) -> Finite n -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> x
from (Finite n -> f x) -> [Finite n] -> [f x]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Finite n]
forall (n :: Nat). KnownNat n => [Finite n]
finites))

coenum :: (Enum x, Decidable f, Divisible f) => f x
coenum :: forall x (f :: * -> *). (Enum x, Decidable f, Divisible f) => f x
coenum = (forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> f x)
-> f x
forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
forall r.
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum (\x -> Finite n
to Finite n -> x
_ -> (x -> Finite n) -> f (Finite n) -> f x
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap x -> Finite n
to (f (Finite n) -> f x) -> f (Finite n) -> f x
forall a b. (a -> b) -> a -> b
$ Clown f (Finite n) (Finite n) -> f (Finite n)
forall {k1} {k2} (f :: k1 -> *) (a :: k1) (b :: k2).
Clown f a b -> f a
runClown (Clown f (Finite n) (Finite n)
forall (n :: Nat) (p :: * -> * -> *).
(KnownNat n, Cartesian p, Cocartesian p) =>
p (Finite n) (Finite n)
describeFinite))

cardinality :: forall x proxy. (Enum x) => proxy x -> Int
cardinality :: forall x (proxy :: * -> *). Enum x => proxy x -> Int
cardinality proxy x
_ = forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum @x (x -> Finite n) -> (Finite n -> x) -> Int
forall (n :: Nat).
KnownNat n =>
(x -> Finite n) -> (Finite n -> x) -> Int
getN
  where
    getN ::forall n. KnownNat n => (x -> Finite n) -> (Finite n -> x) -> Int
    getN :: forall (n :: Nat).
KnownNat n =>
(x -> Finite n) -> (Finite n -> x) -> Int
getN x -> Finite n
_ Finite n -> x
_ = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @n Any n
forall a. HasCallStack => a
undefined)

enumList :: forall x. (Enum x) => [x]
enumList :: forall x. Enum x => [x]
enumList = (forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> [x])
-> [x]
forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
forall r.
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum (\x -> Finite n
_ Finite n -> x
from -> Finite n -> x
from (Finite n -> x) -> [Finite n] -> [x]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Finite n]
forall (n :: Nat). KnownNat n => [Finite n]
finites)

describeEnum :: (Enum x, Cartesian p, Cocartesian p) => p x x
describeEnum :: forall x (p :: * -> * -> *).
(Enum x, Cartesian p, Cocartesian p) =>
p x x
describeEnum = (forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> p x x)
-> p x x
forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
forall r.
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum ((forall (n :: Nat).
  KnownNat n =>
  (x -> Finite n) -> (Finite n -> x) -> p x x)
 -> p x x)
-> (forall (n :: Nat).
    KnownNat n =>
    (x -> Finite n) -> (Finite n -> x) -> p x x)
-> p x x
forall a b. (a -> b) -> a -> b
$ \x -> Finite n
to Finite n -> x
from -> (x -> Finite n)
-> (Finite n -> x) -> p (Finite n) (Finite n) -> p x x
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap x -> Finite n
to Finite n -> x
from p (Finite n) (Finite n)
forall (n :: Nat) (p :: * -> * -> *).
(KnownNat n, Cartesian p, Cocartesian p) =>
p (Finite n) (Finite n)
describeFinite

ptraverseFunction :: forall x p a b. (Enum x, Cartesian p) => p a b -> p (x -> a) (x -> b)
ptraverseFunction :: forall x (p :: * -> * -> *) a b.
(Enum x, Cartesian p) =>
p a b -> p (x -> a) (x -> b)
ptraverseFunction p a b
p = forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum @x ((forall (n :: Nat).
  KnownNat n =>
  (x -> Finite n) -> (Finite n -> x) -> p (x -> a) (x -> b))
 -> p (x -> a) (x -> b))
-> (forall (n :: Nat).
    KnownNat n =>
    (x -> Finite n) -> (Finite n -> x) -> p (x -> a) (x -> b))
-> p (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ \x -> Finite n
to Finite n -> x
from -> ((x -> a) -> Finite n -> a)
-> ((Finite n -> b) -> x -> b)
-> p (Finite n -> a) (Finite n -> b)
-> p (x -> a) (x -> b)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((x -> a) -> (Finite n -> x) -> Finite n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> x
from) ((Finite n -> b) -> (x -> Finite n) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Finite n
to) (p a b -> p (Finite n -> a) (Finite n -> b)
forall (n :: Nat) a b.
KnownNat n =>
p a b -> p (Finite n -> a) (Finite n -> b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
p a b -> p (Finite n -> a) (Finite n -> b)
proPower p a b
p)

instance Enum Void
instance Enum ()
instance (Enum x, Enum y) => Enum (Either x y) where
  enumeration :: FinFn (Either x y) (Either x y)
enumeration = FinFn x x
forall x. Enum x => FinFn x x
enumeration FinFn x x -> FinFn y y -> FinFn (Either x y) (Either x y)
forall a b a' b'.
FinFn a b -> FinFn a' b' -> FinFn (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ FinFn y y
forall x. Enum x => FinFn x x
enumeration
  withEnum :: forall r.
(forall (n :: Nat).
 KnownNat n =>
 (Either x y -> Finite n) -> (Finite n -> Either x y) -> r)
-> r
withEnum = FinFn (Either x y) (Either x y)
-> (forall (n :: Nat).
    KnownNat n =>
    (Either x y -> Finite n) -> (Finite n -> Either x y) -> r)
-> r
forall a b r.
FinFn a b
-> (forall (n :: Nat).
    KnownNat n =>
    (a -> Finite n) -> (Finite n -> b) -> r)
-> r
withFinFn FinFn (Either x y) (Either x y)
forall x. Enum x => FinFn x x
enumeration

instance (Enum x, Enum y) => Enum (x,y) where
  enumeration :: FinFn (x, y) (x, y)
enumeration = FinFn x x
forall x. Enum x => FinFn x x
enumeration FinFn x x -> FinFn y y -> FinFn (x, y) (x, y)
forall a b a' b'. FinFn a b -> FinFn a' b' -> FinFn (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** FinFn y y
forall x. Enum x => FinFn x x
enumeration
  withEnum :: forall r.
(forall (n :: Nat).
 KnownNat n =>
 ((x, y) -> Finite n) -> (Finite n -> (x, y)) -> r)
-> r
withEnum = FinFn (x, y) (x, y)
-> (forall (n :: Nat).
    KnownNat n =>
    ((x, y) -> Finite n) -> (Finite n -> (x, y)) -> r)
-> r
forall a b r.
FinFn a b
-> (forall (n :: Nat).
    KnownNat n =>
    (a -> Finite n) -> (Finite n -> b) -> r)
-> r
withFinFn FinFn (x, y) (x, y)
forall x. Enum x => FinFn x x
enumeration

instance (Enum x1, Enum x2, Enum x3)=> Enum (x1,x2,x3) where
  enumeration :: FinFn (x1, x2, x3) (x1, x2, x3)
enumeration = ((x1, x2, x3) -> (x1, (x2, x3)))
-> ((x1, (x2, x3)) -> (x1, x2, x3))
-> FinFn x1 x1
-> FinFn (x2, x3) (x2, x3)
-> FinFn (x1, x2, x3) (x1, x2, x3)
forall a a1 a2 b1 b2 b.
(a -> (a1, a2))
-> ((b1, b2) -> b) -> FinFn a1 b1 -> FinFn a2 b2 -> FinFn a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
proProduct (x1, x2, x3) -> (x1, (x2, x3))
forall {a} {a} {b}. (a, a, b) -> (a, (a, b))
from (x1, (x2, x3)) -> (x1, x2, x3)
forall {a} {b} {c}. (a, (b, c)) -> (a, b, c)
to FinFn x1 x1
forall x. Enum x => FinFn x x
enumeration FinFn (x2, x3) (x2, x3)
forall x. Enum x => FinFn x x
enumeration where
    from :: (a, a, b) -> (a, (a, b))
from (a
x1,a
x2,b
x3) = (a
x1,(a
x2,b
x3))
    to :: (a, (b, c)) -> (a, b, c)
to (a
x1,(b
x2,c
x3)) = (a
x1,b
x2,c
x3)
  withEnum :: forall r.
(forall (n :: Nat).
 KnownNat n =>
 ((x1, x2, x3) -> Finite n) -> (Finite n -> (x1, x2, x3)) -> r)
-> r
withEnum = FinFn (x1, x2, x3) (x1, x2, x3)
-> (forall (n :: Nat).
    KnownNat n =>
    ((x1, x2, x3) -> Finite n) -> (Finite n -> (x1, x2, x3)) -> r)
-> r
forall a b r.
FinFn a b
-> (forall (n :: Nat).
    KnownNat n =>
    (a -> Finite n) -> (Finite n -> b) -> r)
-> r
withFinFn FinFn (x1, x2, x3) (x1, x2, x3)
forall x. Enum x => FinFn x x
enumeration
instance (Enum x1, Enum x2, Enum x3, Enum x4) => Enum (x1,x2,x3,x4) where
  enumeration :: FinFn (x1, x2, x3, x4) (x1, x2, x3, x4)
enumeration = ((x1, x2, x3, x4) -> ((x1, x2), (x3, x4)))
-> (((x1, x2), (x3, x4)) -> (x1, x2, x3, x4))
-> FinFn (x1, x2) (x1, x2)
-> FinFn (x3, x4) (x3, x4)
-> FinFn (x1, x2, x3, x4) (x1, x2, x3, x4)
forall a a1 a2 b1 b2 b.
(a -> (a1, a2))
-> ((b1, b2) -> b) -> FinFn a1 b1 -> FinFn a2 b2 -> FinFn a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
proProduct (x1, x2, x3, x4) -> ((x1, x2), (x3, x4))
forall {a} {b} {a} {b}. (a, b, a, b) -> ((a, b), (a, b))
from ((x1, x2), (x3, x4)) -> (x1, x2, x3, x4)
forall {a} {b} {c} {d}. ((a, b), (c, d)) -> (a, b, c, d)
to FinFn (x1, x2) (x1, x2)
forall x. Enum x => FinFn x x
enumeration FinFn (x3, x4) (x3, x4)
forall x. Enum x => FinFn x x
enumeration where
    from :: (a, b, a, b) -> ((a, b), (a, b))
from (a
x1,b
x2,a
x3,b
x4) = ((a
x1,b
x2),(a
x3,b
x4))
    to :: ((a, b), (c, d)) -> (a, b, c, d)
to ((a
x1,b
x2),(c
x3,d
x4)) = (a
x1,b
x2,c
x3,d
x4)
  withEnum :: forall r.
(forall (n :: Nat).
 KnownNat n =>
 ((x1, x2, x3, x4) -> Finite n)
 -> (Finite n -> (x1, x2, x3, x4)) -> r)
-> r
withEnum = FinFn (x1, x2, x3, x4) (x1, x2, x3, x4)
-> (forall (n :: Nat).
    KnownNat n =>
    ((x1, x2, x3, x4) -> Finite n)
    -> (Finite n -> (x1, x2, x3, x4)) -> r)
-> r
forall a b r.
FinFn a b
-> (forall (n :: Nat).
    KnownNat n =>
    (a -> Finite n) -> (Finite n -> b) -> r)
-> r
withFinFn FinFn (x1, x2, x3, x4) (x1, x2, x3, x4)
forall x. Enum x => FinFn x x
enumeration
instance Enum Bool
instance Enum Ordering
instance Enum x => Enum (Maybe x) where
  withEnum :: forall r.
(forall (n :: Nat).
 KnownNat n =>
 (Maybe x -> Finite n) -> (Finite n -> Maybe x) -> r)
-> r
withEnum forall (n :: Nat).
KnownNat n =>
(Maybe x -> Finite n) -> (Finite n -> Maybe x) -> r
k = forall x r.
Enum x =>
(forall (n :: Nat).
 KnownNat n =>
 (x -> Finite n) -> (Finite n -> x) -> r)
-> r
withEnum @x (\x -> Finite n
from Finite n -> x
to -> (Maybe x -> Finite (n + 1)) -> (Finite (n + 1) -> Maybe x) -> r
forall (n :: Nat).
KnownNat n =>
(Maybe x -> Finite n) -> (Finite n -> Maybe x) -> r
k (Finite (n + 1)
-> (x -> Finite (n + 1)) -> Maybe x -> Finite (n + 1)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Finite (n + 1)
forall a. Bounded a => a
minBound (Finite n -> Finite (n + 1)
forall (n :: Nat). Finite n -> Finite (n + 1)
shift (Finite n -> Finite (n + 1))
-> (x -> Finite n) -> x -> Finite (n + 1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Finite n
from)) ((Finite n -> x) -> Maybe (Finite n) -> Maybe x
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Finite n -> x
to (Maybe (Finite n) -> Maybe x)
-> (Finite (n + 1) -> Maybe (Finite n))
-> Finite (n + 1)
-> Maybe x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (n + 1) -> Maybe (Finite n)
forall (n :: Nat). Finite (n + 1) -> Maybe (Finite n)
unshift))

instance Enum Word8
instance Enum Word16
instance Enum Word32
instance Enum Word64
instance Enum Word

instance Enum Int8
instance Enum Int16
instance Enum Int32
instance Enum Int64
instance Enum Int

instance Enum Char