{-# LANGUAGE
    DataKinds
  , DeriveDataTypeable
  , DeriveGeneric
  , DerivingVia
  , FlexibleContexts
  , FlexibleInstances
  , GADTs
  , GeneralizedNewtypeDeriving
  , MultiParamTypeClasses
  , PatternSynonyms
  , PolyKinds
  , ScopedTypeVariables
  , StandaloneDeriving
  , TypeApplications
  , TypeFamilies
  , TypeOperators
  , ViewPatterns
#-}

{-|
Module: Data.Group.Cyclic

Cyclic groups: integers modulo @n@ (clock arithmetic).
-}

module Data.Group.Cyclic
  ( Cyclic(Cyclic), getCyclic
  , C, Z
  , CyclicEnum(..)
  , pattern Involution, involution
  , rootOfUnity
  )
  where

-- base

import Data.Coerce
  ( coerce )
import Data.Complex
  ( Complex(..), conjugate, mkPolar )
import Data.Data
  ( Data )
import Data.Monoid
  ( Sum(..), Product(..) )
import Data.Proxy
  ( Proxy(..) )
import GHC.Generics
  ( Generic, Generic1 )
import GHC.TypeNats
  ( Nat, KnownNat, natVal
  , type (<=)
  )

-- deepseq

import Control.DeepSeq
  ( NFData )

-- finite-typelits

import Data.Finite
  ( Finite, getFinite )

-- acts

import Data.Act
  ( Act(..), Torsor(..) )
import Data.Group
  ( Group(..) )

-----------------------------------------------------------------


-- | Cyclic group of order @n@: integers with addition modulo @n@.

newtype Cyclic n = MkCyclic { Cyclic n -> Finite n
runCyclic :: Finite n }
  deriving stock   ( Int -> Cyclic n -> ShowS
[Cyclic n] -> ShowS
Cyclic n -> String
(Int -> Cyclic n -> ShowS)
-> (Cyclic n -> String) -> ([Cyclic n] -> ShowS) -> Show (Cyclic n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat). Int -> Cyclic n -> ShowS
forall (n :: Nat). [Cyclic n] -> ShowS
forall (n :: Nat). Cyclic n -> String
showList :: [Cyclic n] -> ShowS
$cshowList :: forall (n :: Nat). [Cyclic n] -> ShowS
show :: Cyclic n -> String
$cshow :: forall (n :: Nat). Cyclic n -> String
showsPrec :: Int -> Cyclic n -> ShowS
$cshowsPrec :: forall (n :: Nat). Int -> Cyclic n -> ShowS
Show, (forall x. Cyclic n -> Rep (Cyclic n) x)
-> (forall x. Rep (Cyclic n) x -> Cyclic n) -> Generic (Cyclic n)
forall x. Rep (Cyclic n) x -> Cyclic n
forall x. Cyclic n -> Rep (Cyclic n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) x. Rep (Cyclic n) x -> Cyclic n
forall (n :: Nat) x. Cyclic n -> Rep (Cyclic n) x
$cto :: forall (n :: Nat) x. Rep (Cyclic n) x -> Cyclic n
$cfrom :: forall (n :: Nat) x. Cyclic n -> Rep (Cyclic n) x
Generic, (forall (a :: Nat). Cyclic a -> Rep1 Cyclic a)
-> (forall (a :: Nat). Rep1 Cyclic a -> Cyclic a)
-> Generic1 Cyclic
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall (a :: Nat). Rep1 Cyclic a -> Cyclic a
forall (a :: Nat). Cyclic a -> Rep1 Cyclic a
$cto1 :: forall (a :: Nat). Rep1 Cyclic a -> Cyclic a
$cfrom1 :: forall (a :: Nat). Cyclic a -> Rep1 Cyclic a
Generic1 )
  deriving newtype ( Cyclic n -> Cyclic n -> Bool
(Cyclic n -> Cyclic n -> Bool)
-> (Cyclic n -> Cyclic n -> Bool) -> Eq (Cyclic n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: Nat). Cyclic n -> Cyclic n -> Bool
/= :: Cyclic n -> Cyclic n -> Bool
$c/= :: forall (n :: Nat). Cyclic n -> Cyclic n -> Bool
== :: Cyclic n -> Cyclic n -> Bool
$c== :: forall (n :: Nat). Cyclic n -> Cyclic n -> Bool
Eq, Eq (Cyclic n)
Eq (Cyclic n)
-> (Cyclic n -> Cyclic n -> Ordering)
-> (Cyclic n -> Cyclic n -> Bool)
-> (Cyclic n -> Cyclic n -> Bool)
-> (Cyclic n -> Cyclic n -> Bool)
-> (Cyclic n -> Cyclic n -> Bool)
-> (Cyclic n -> Cyclic n -> Cyclic n)
-> (Cyclic n -> Cyclic n -> Cyclic n)
-> Ord (Cyclic n)
Cyclic n -> Cyclic n -> Bool
Cyclic n -> Cyclic n -> Ordering
Cyclic n -> Cyclic n -> Cyclic n
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (n :: Nat). Eq (Cyclic n)
forall (n :: Nat). Cyclic n -> Cyclic n -> Bool
forall (n :: Nat). Cyclic n -> Cyclic n -> Ordering
forall (n :: Nat). Cyclic n -> Cyclic n -> Cyclic n
min :: Cyclic n -> Cyclic n -> Cyclic n
$cmin :: forall (n :: Nat). Cyclic n -> Cyclic n -> Cyclic n
max :: Cyclic n -> Cyclic n -> Cyclic n
$cmax :: forall (n :: Nat). Cyclic n -> Cyclic n -> Cyclic n
>= :: Cyclic n -> Cyclic n -> Bool
$c>= :: forall (n :: Nat). Cyclic n -> Cyclic n -> Bool
> :: Cyclic n -> Cyclic n -> Bool
$c> :: forall (n :: Nat). Cyclic n -> Cyclic n -> Bool
<= :: Cyclic n -> Cyclic n -> Bool
$c<= :: forall (n :: Nat). Cyclic n -> Cyclic n -> Bool
< :: Cyclic n -> Cyclic n -> Bool
$c< :: forall (n :: Nat). Cyclic n -> Cyclic n -> Bool
compare :: Cyclic n -> Cyclic n -> Ordering
$ccompare :: forall (n :: Nat). Cyclic n -> Cyclic n -> Ordering
$cp1Ord :: forall (n :: Nat). Eq (Cyclic n)
Ord, Int -> Cyclic n
Cyclic n -> Int
Cyclic n -> [Cyclic n]
Cyclic n -> Cyclic n
Cyclic n -> Cyclic n -> [Cyclic n]
Cyclic n -> Cyclic n -> Cyclic n -> [Cyclic n]
(Cyclic n -> Cyclic n)
-> (Cyclic n -> Cyclic n)
-> (Int -> Cyclic n)
-> (Cyclic n -> Int)
-> (Cyclic n -> [Cyclic n])
-> (Cyclic n -> Cyclic n -> [Cyclic n])
-> (Cyclic n -> Cyclic n -> [Cyclic n])
-> (Cyclic n -> Cyclic n -> Cyclic n -> [Cyclic n])
-> Enum (Cyclic n)
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
forall (n :: Nat). KnownNat n => Int -> Cyclic n
forall (n :: Nat). KnownNat n => Cyclic n -> Int
forall (n :: Nat). KnownNat n => Cyclic n -> [Cyclic n]
forall (n :: Nat). KnownNat n => Cyclic n -> Cyclic n
forall (n :: Nat). KnownNat n => Cyclic n -> Cyclic n -> [Cyclic n]
forall (n :: Nat).
KnownNat n =>
Cyclic n -> Cyclic n -> Cyclic n -> [Cyclic n]
enumFromThenTo :: Cyclic n -> Cyclic n -> Cyclic n -> [Cyclic n]
$cenumFromThenTo :: forall (n :: Nat).
KnownNat n =>
Cyclic n -> Cyclic n -> Cyclic n -> [Cyclic n]
enumFromTo :: Cyclic n -> Cyclic n -> [Cyclic n]
$cenumFromTo :: forall (n :: Nat). KnownNat n => Cyclic n -> Cyclic n -> [Cyclic n]
enumFromThen :: Cyclic n -> Cyclic n -> [Cyclic n]
$cenumFromThen :: forall (n :: Nat). KnownNat n => Cyclic n -> Cyclic n -> [Cyclic n]
enumFrom :: Cyclic n -> [Cyclic n]
$cenumFrom :: forall (n :: Nat). KnownNat n => Cyclic n -> [Cyclic n]
fromEnum :: Cyclic n -> Int
$cfromEnum :: forall (n :: Nat). KnownNat n => Cyclic n -> Int
toEnum :: Int -> Cyclic n
$ctoEnum :: forall (n :: Nat). KnownNat n => Int -> Cyclic n
pred :: Cyclic n -> Cyclic n
$cpred :: forall (n :: Nat). KnownNat n => Cyclic n -> Cyclic n
succ :: Cyclic n -> Cyclic n
$csucc :: forall (n :: Nat). KnownNat n => Cyclic n -> Cyclic n
Enum, Cyclic n
Cyclic n -> Cyclic n -> Bounded (Cyclic n)
forall a. a -> a -> Bounded a
forall (n :: Nat). KnownNat n => Cyclic n
maxBound :: Cyclic n
$cmaxBound :: forall (n :: Nat). KnownNat n => Cyclic n
minBound :: Cyclic n
$cminBound :: forall (n :: Nat). KnownNat n => Cyclic n
Bounded, Cyclic n -> ()
(Cyclic n -> ()) -> NFData (Cyclic n)
forall a. (a -> ()) -> NFData a
forall (n :: Nat). Cyclic n -> ()
rnf :: Cyclic n -> ()
$crnf :: forall (n :: Nat). Cyclic n -> ()
NFData )
deriving via ( Sum ( Finite n ) ) instance KnownNat n => Semigroup ( Cyclic n ) 
deriving via ( Sum ( Finite n ) ) instance ( KnownNat n, 1 <= n ) => Monoid ( Cyclic n )
deriving via ( Sum ( Finite n ) ) instance ( KnownNat n, 1 <= n ) => Group  ( Cyclic n )

{-# COMPLETE Cyclic #-}
-- | Smart pattern and constructor for elements of cyclic groups.

pattern Cyclic :: forall n. KnownNat n => Int -> Cyclic n
pattern $bCyclic :: Int -> Cyclic n
$mCyclic :: forall r (n :: Nat).
KnownNat n =>
Cyclic n -> (Int -> r) -> (Void# -> r) -> r
Cyclic i <- ( fromIntegral . getFinite . runCyclic -> i )
  where
    Cyclic Int
i = Finite n -> Cyclic n
forall (n :: Nat). Finite n -> Cyclic n
MkCyclic ( Int -> Finite n
forall a b. (Integral a, Num b) => a -> b
fromIntegral ( Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` ( Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ( Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal ( Proxy n
forall k (t :: k). Proxy t
Proxy @n ) ) ) ) )

-- | Obtain a representative in the range \( [0, n[ \).

getCyclic :: forall n. KnownNat n => Cyclic n -> Int
getCyclic :: Cyclic n -> Int
getCyclic ( Cyclic Int
i ) = Int
i

-- | Synonym for finite cyclic group.

type C ( n :: Nat ) = Cyclic n
-- | Synonym for infinite cyclic group.

type Z = Sum Int

instance KnownNat n => Act ( Cyclic n ) Int where
  act :: Cyclic n -> Int -> Int
act ( Cyclic Int
f ) Int
j
    | Int
r Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n
    = ( Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n ) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j
    | Bool
otherwise
    = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j
    where
      i, n, r :: Int
      i :: Int
i = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
f
      n :: Int
n = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ( Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal ( Proxy n
forall k (t :: k). Proxy t
Proxy @n ) )
      r :: Int
r = Int
j Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n

-- | Nontrivial element of cyclic group of order 2.

pattern Involution :: Cyclic 2
pattern $bInvolution :: Cyclic 2
$mInvolution :: forall r. Cyclic 2 -> (Void# -> r) -> (Void# -> r) -> r
Involution = Cyclic 1

-- | Act by an involution.

involution :: Act ( Cyclic 2 ) x => x -> x
involution :: x -> x
involution = Cyclic 2 -> x -> x
forall s x. Act s x => s -> x -> x
act Cyclic 2
Involution

instance Act ( Cyclic 2 ) Bool where
  act :: Cyclic 2 -> Bool -> Bool
act Cyclic 2
Involution = Bool -> Bool
not
  act Cyclic 2
_          = Bool -> Bool
forall a. a -> a
id

instance Num i => Act ( Cyclic 2 ) ( Sum i ) where
  act :: Cyclic 2 -> Sum i -> Sum i
act Cyclic 2
Involution = (i -> i) -> Sum i -> Sum i
coerce ( i -> i
forall a. Num a => a -> a
negate :: i -> i )
  act Cyclic 2
_          = Sum i -> Sum i
forall a. a -> a
id

instance Fractional i => Act ( Cyclic 2 ) ( Product i ) where
  act :: Cyclic 2 -> Product i -> Product i
act Cyclic 2
Involution = (i -> i) -> Product i -> Product i
coerce ( i -> i
forall a. Fractional a => a -> a
recip :: i -> i )
  act Cyclic 2
_          = Product i -> Product i
forall a. a -> a
id

instance Num a => Act ( Cyclic 2 ) ( Complex a ) where
  act :: Cyclic 2 -> Complex a -> Complex a
act Cyclic 2
Involution = Complex a -> Complex a
forall a. Num a => Complex a -> Complex a
conjugate
  act Cyclic 2
_          = Complex a -> Complex a
forall a. a -> a
id

-- | Natural complex representations of finite cyclic groups as roots of unity.

rootOfUnity :: forall a n. ( KnownNat n, Floating a ) => Cyclic n -> Complex a
rootOfUnity :: Cyclic n -> Complex a
rootOfUnity ( Cyclic Int
f ) = a -> a -> Complex a
forall a. Floating a => a -> a -> Complex a
mkPolar a
1 ( a
2 a -> a -> a
forall a. Num a => a -> a -> a
* a
forall a. Floating a => a
pi a -> a -> a
forall a. Num a => a -> a -> a
* a
i a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
n )
  where
    i, n :: a
    i :: a
i = Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
f
    n :: a
n = Natural -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral ( Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal ( Proxy n
forall k (t :: k). Proxy t
Proxy @n ) )

-- | Newtype for cycling through elements in a finite enumeration.

--

-- > data ABCD = A | B | C | D 

-- >   deriving stock ( Enum, Bounded )

-- >   deriving ( Act ( Cyclic 4 ), Torsor ( Cyclic 4 ) )

-- >     via CyclicEnum ABCD

-- 

-- > > act ( Cyclic 2 ) C

-- > A

--

-- > > act ( Cyclic (-1) ) A

-- > D

--

-- > > ( C --> B :: Cyclic 4 )

-- > Cyclic 3

--

-- __Warning__

-- It is unfortunately not checked that the size of the group

-- matches the size of the finite enumeration.

-- Please manually ensure this condition.

newtype CyclicEnum a = CyclicEnum { CyclicEnum a -> a
getCyclicEnum :: a }
  deriving stock   ( Int -> CyclicEnum a -> ShowS
[CyclicEnum a] -> ShowS
CyclicEnum a -> String
(Int -> CyclicEnum a -> ShowS)
-> (CyclicEnum a -> String)
-> ([CyclicEnum a] -> ShowS)
-> Show (CyclicEnum a)
forall a. Show a => Int -> CyclicEnum a -> ShowS
forall a. Show a => [CyclicEnum a] -> ShowS
forall a. Show a => CyclicEnum a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CyclicEnum a] -> ShowS
$cshowList :: forall a. Show a => [CyclicEnum a] -> ShowS
show :: CyclicEnum a -> String
$cshow :: forall a. Show a => CyclicEnum a -> String
showsPrec :: Int -> CyclicEnum a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> CyclicEnum a -> ShowS
Show, Typeable (CyclicEnum a)
DataType
Constr
Typeable (CyclicEnum a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CyclicEnum a -> c (CyclicEnum a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (CyclicEnum a))
-> (CyclicEnum a -> Constr)
-> (CyclicEnum a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (CyclicEnum a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (CyclicEnum a)))
-> ((forall b. Data b => b -> b) -> CyclicEnum a -> CyclicEnum a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r)
-> (forall u. (forall d. Data d => d -> u) -> CyclicEnum a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> CyclicEnum a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a))
-> Data (CyclicEnum a)
CyclicEnum a -> DataType
CyclicEnum a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (CyclicEnum a))
(forall b. Data b => b -> b) -> CyclicEnum a -> CyclicEnum a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CyclicEnum a -> c (CyclicEnum a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CyclicEnum a)
forall a. Data a => Typeable (CyclicEnum a)
forall a. Data a => CyclicEnum a -> DataType
forall a. Data a => CyclicEnum a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> CyclicEnum a -> CyclicEnum a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> CyclicEnum a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> CyclicEnum a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CyclicEnum a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CyclicEnum a -> c (CyclicEnum a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (CyclicEnum a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CyclicEnum a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CyclicEnum a -> u
forall u. (forall d. Data d => d -> u) -> CyclicEnum a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CyclicEnum a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CyclicEnum a -> c (CyclicEnum a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (CyclicEnum a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CyclicEnum a))
$cCyclicEnum :: Constr
$tCyclicEnum :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
gmapMp :: (forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
gmapM :: (forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> CyclicEnum a -> m (CyclicEnum a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> CyclicEnum a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> CyclicEnum a -> u
gmapQ :: (forall d. Data d => d -> u) -> CyclicEnum a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> CyclicEnum a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CyclicEnum a -> r
gmapT :: (forall b. Data b => b -> b) -> CyclicEnum a -> CyclicEnum a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> CyclicEnum a -> CyclicEnum a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CyclicEnum a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CyclicEnum a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (CyclicEnum a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (CyclicEnum a))
dataTypeOf :: CyclicEnum a -> DataType
$cdataTypeOf :: forall a. Data a => CyclicEnum a -> DataType
toConstr :: CyclicEnum a -> Constr
$ctoConstr :: forall a. Data a => CyclicEnum a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CyclicEnum a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CyclicEnum a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CyclicEnum a -> c (CyclicEnum a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CyclicEnum a -> c (CyclicEnum a)
$cp1Data :: forall a. Data a => Typeable (CyclicEnum a)
Data, (forall x. CyclicEnum a -> Rep (CyclicEnum a) x)
-> (forall x. Rep (CyclicEnum a) x -> CyclicEnum a)
-> Generic (CyclicEnum a)
forall x. Rep (CyclicEnum a) x -> CyclicEnum a
forall x. CyclicEnum a -> Rep (CyclicEnum a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (CyclicEnum a) x -> CyclicEnum a
forall a x. CyclicEnum a -> Rep (CyclicEnum a) x
$cto :: forall a x. Rep (CyclicEnum a) x -> CyclicEnum a
$cfrom :: forall a x. CyclicEnum a -> Rep (CyclicEnum a) x
Generic, (forall a. CyclicEnum a -> Rep1 CyclicEnum a)
-> (forall a. Rep1 CyclicEnum a -> CyclicEnum a)
-> Generic1 CyclicEnum
forall a. Rep1 CyclicEnum a -> CyclicEnum a
forall a. CyclicEnum a -> Rep1 CyclicEnum a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall a. Rep1 CyclicEnum a -> CyclicEnum a
$cfrom1 :: forall a. CyclicEnum a -> Rep1 CyclicEnum a
Generic1 )
  deriving newtype ( CyclicEnum a -> CyclicEnum a -> Bool
(CyclicEnum a -> CyclicEnum a -> Bool)
-> (CyclicEnum a -> CyclicEnum a -> Bool) -> Eq (CyclicEnum a)
forall a. Eq a => CyclicEnum a -> CyclicEnum a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CyclicEnum a -> CyclicEnum a -> Bool
$c/= :: forall a. Eq a => CyclicEnum a -> CyclicEnum a -> Bool
== :: CyclicEnum a -> CyclicEnum a -> Bool
$c== :: forall a. Eq a => CyclicEnum a -> CyclicEnum a -> Bool
Eq, Eq (CyclicEnum a)
Eq (CyclicEnum a)
-> (CyclicEnum a -> CyclicEnum a -> Ordering)
-> (CyclicEnum a -> CyclicEnum a -> Bool)
-> (CyclicEnum a -> CyclicEnum a -> Bool)
-> (CyclicEnum a -> CyclicEnum a -> Bool)
-> (CyclicEnum a -> CyclicEnum a -> Bool)
-> (CyclicEnum a -> CyclicEnum a -> CyclicEnum a)
-> (CyclicEnum a -> CyclicEnum a -> CyclicEnum a)
-> Ord (CyclicEnum a)
CyclicEnum a -> CyclicEnum a -> Bool
CyclicEnum a -> CyclicEnum a -> Ordering
CyclicEnum a -> CyclicEnum a -> CyclicEnum a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (CyclicEnum a)
forall a. Ord a => CyclicEnum a -> CyclicEnum a -> Bool
forall a. Ord a => CyclicEnum a -> CyclicEnum a -> Ordering
forall a. Ord a => CyclicEnum a -> CyclicEnum a -> CyclicEnum a
min :: CyclicEnum a -> CyclicEnum a -> CyclicEnum a
$cmin :: forall a. Ord a => CyclicEnum a -> CyclicEnum a -> CyclicEnum a
max :: CyclicEnum a -> CyclicEnum a -> CyclicEnum a
$cmax :: forall a. Ord a => CyclicEnum a -> CyclicEnum a -> CyclicEnum a
>= :: CyclicEnum a -> CyclicEnum a -> Bool
$c>= :: forall a. Ord a => CyclicEnum a -> CyclicEnum a -> Bool
> :: CyclicEnum a -> CyclicEnum a -> Bool
$c> :: forall a. Ord a => CyclicEnum a -> CyclicEnum a -> Bool
<= :: CyclicEnum a -> CyclicEnum a -> Bool
$c<= :: forall a. Ord a => CyclicEnum a -> CyclicEnum a -> Bool
< :: CyclicEnum a -> CyclicEnum a -> Bool
$c< :: forall a. Ord a => CyclicEnum a -> CyclicEnum a -> Bool
compare :: CyclicEnum a -> CyclicEnum a -> Ordering
$ccompare :: forall a. Ord a => CyclicEnum a -> CyclicEnum a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (CyclicEnum a)
Ord, Int -> CyclicEnum a
CyclicEnum a -> Int
CyclicEnum a -> [CyclicEnum a]
CyclicEnum a -> CyclicEnum a
CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
CyclicEnum a -> CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
(CyclicEnum a -> CyclicEnum a)
-> (CyclicEnum a -> CyclicEnum a)
-> (Int -> CyclicEnum a)
-> (CyclicEnum a -> Int)
-> (CyclicEnum a -> [CyclicEnum a])
-> (CyclicEnum a -> CyclicEnum a -> [CyclicEnum a])
-> (CyclicEnum a -> CyclicEnum a -> [CyclicEnum a])
-> (CyclicEnum a -> CyclicEnum a -> CyclicEnum a -> [CyclicEnum a])
-> Enum (CyclicEnum a)
forall a. Enum a => Int -> CyclicEnum a
forall a. Enum a => CyclicEnum a -> Int
forall a. Enum a => CyclicEnum a -> [CyclicEnum a]
forall a. Enum a => CyclicEnum a -> CyclicEnum a
forall a. Enum a => CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
forall a.
Enum a =>
CyclicEnum a -> CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: CyclicEnum a -> CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
$cenumFromThenTo :: forall a.
Enum a =>
CyclicEnum a -> CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
enumFromTo :: CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
$cenumFromTo :: forall a. Enum a => CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
enumFromThen :: CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
$cenumFromThen :: forall a. Enum a => CyclicEnum a -> CyclicEnum a -> [CyclicEnum a]
enumFrom :: CyclicEnum a -> [CyclicEnum a]
$cenumFrom :: forall a. Enum a => CyclicEnum a -> [CyclicEnum a]
fromEnum :: CyclicEnum a -> Int
$cfromEnum :: forall a. Enum a => CyclicEnum a -> Int
toEnum :: Int -> CyclicEnum a
$ctoEnum :: forall a. Enum a => Int -> CyclicEnum a
pred :: CyclicEnum a -> CyclicEnum a
$cpred :: forall a. Enum a => CyclicEnum a -> CyclicEnum a
succ :: CyclicEnum a -> CyclicEnum a
$csucc :: forall a. Enum a => CyclicEnum a -> CyclicEnum a
Enum, CyclicEnum a
CyclicEnum a -> CyclicEnum a -> Bounded (CyclicEnum a)
forall a. a -> a -> Bounded a
forall a. Bounded a => CyclicEnum a
maxBound :: CyclicEnum a
$cmaxBound :: forall a. Bounded a => CyclicEnum a
minBound :: CyclicEnum a
$cminBound :: forall a. Bounded a => CyclicEnum a
Bounded, CyclicEnum a -> ()
(CyclicEnum a -> ()) -> NFData (CyclicEnum a)
forall a. NFData a => CyclicEnum a -> ()
forall a. (a -> ()) -> NFData a
rnf :: CyclicEnum a -> ()
$crnf :: forall a. NFData a => CyclicEnum a -> ()
NFData )

instance ( Enum a, Bounded a, KnownNat n ) => Act ( Cyclic n ) ( CyclicEnum a ) where
  act :: Cyclic n -> CyclicEnum a -> CyclicEnum a
act ( Cyclic Int
f ) CyclicEnum a
a = Int -> CyclicEnum a
forall a. Enum a => Int -> a
toEnum Int
j
    where
      b_min, b_max, i, j :: Int
      b_min :: Int
b_min = a -> Int
forall a. Enum a => a -> Int
fromEnum ( Bounded a => a
forall a. Bounded a => a
minBound @a )
      b_max :: Int
b_max = a -> Int
forall a. Enum a => a -> Int
fromEnum ( Bounded a => a
forall a. Bounded a => a
maxBound @a )
      i :: Int
i = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
f
      j :: Int
j = Int
b_min Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ( CyclicEnum a -> Int
forall a. Enum a => a -> Int
fromEnum CyclicEnum a
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b_min ) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` ( Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b_max Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b_min )
      -- Assumes n ~ ( 1 + b_max - b_min ).

instance ( Enum a, Bounded a, KnownNat n, 1 <= n ) => Torsor ( Cyclic n ) ( CyclicEnum a ) where
  CyclicEnum a
a --> :: CyclicEnum a -> CyclicEnum a -> Cyclic n
--> CyclicEnum a
b = Int -> Cyclic n
forall (n :: Nat). KnownNat n => Int -> Cyclic n
Cyclic (Int -> Cyclic n) -> (Int -> Int) -> Int -> Cyclic n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n ) (Int -> Cyclic n) -> Int -> Cyclic n
forall a b. (a -> b) -> a -> b
$ CyclicEnum a -> Int
forall a. Enum a => a -> Int
fromEnum CyclicEnum a
b Int -> Int -> Int
forall a. Num a => a -> a -> a
- CyclicEnum a -> Int
forall a. Enum a => a -> Int
fromEnum CyclicEnum a
a
    where
      n :: Int
      n :: Int
n = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ( Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal ( Proxy n
forall k (t :: k). Proxy t
Proxy @n ) )