-- |
-- Module:      Math.NumberTheory.Moduli.Singleton
-- Copyright:   (c) 2019 Andrew Lelechenko
-- Licence:     MIT
-- Maintainer:  Andrew Lelechenko <andrew.lelechenko@gmail.com>
--
-- Singleton data types.
--

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE ViewPatterns        #-}

module Math.NumberTheory.Moduli.Singleton
  ( -- * SFactors singleton
    SFactors
  , sfactors
  , someSFactors
  , unSFactors
  , proofFromSFactors
    -- * CyclicGroup singleton
  , CyclicGroup
  , cyclicGroup
  , cyclicGroupFromFactors
  , cyclicGroupFromModulo
  , proofFromCyclicGroup
  , pattern CG2
  , pattern CG4
  , pattern CGOddPrimePower
  , pattern CGDoubleOddPrimePower
    -- * SFactors \<=\> CyclicGroup
  , cyclicGroupToSFactors
  , sfactorsToCyclicGroup
    -- * Some wrapper
  , Some(..)
  ) where

import Control.DeepSeq
import Data.Constraint
import Data.Kind
import Data.List (sort)
import qualified Data.Map as M
import Data.Proxy
#if __GLASGOW_HASKELL__ < 803
import Data.Semigroup
#endif
import GHC.Generics
import GHC.TypeNats (KnownNat, Nat, natVal)
import Numeric.Natural
import Unsafe.Coerce

import Math.NumberTheory.Roots (highestPower)
import Math.NumberTheory.Primes
import Math.NumberTheory.Primes.Types
import Math.NumberTheory.Utils.FromIntegral

-- | Wrapper to hide an unknown type-level natural.
data Some (a :: Nat -> Type) where
  Some :: a m -> Some a

-- | From "Data.Constraint.Nat".
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))

-- | This singleton data type establishes a correspondence
-- between a modulo @m@ on type level
-- and its factorisation on term level.
newtype SFactors a (m :: Nat) = SFactors
  { SFactors a m -> [(Prime a, Word)]
unSFactors :: [(Prime a, Word)]
  -- ^ Factors of @m@.
  } deriving (Int -> SFactors a m -> ShowS
[SFactors a m] -> ShowS
SFactors a m -> String
(Int -> SFactors a m -> ShowS)
-> (SFactors a m -> String)
-> ([SFactors a m] -> ShowS)
-> Show (SFactors a m)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a (m :: Nat). Show a => Int -> SFactors a m -> ShowS
forall a (m :: Nat). Show a => [SFactors a m] -> ShowS
forall a (m :: Nat). Show a => SFactors a m -> String
showList :: [SFactors a m] -> ShowS
$cshowList :: forall a (m :: Nat). Show a => [SFactors a m] -> ShowS
show :: SFactors a m -> String
$cshow :: forall a (m :: Nat). Show a => SFactors a m -> String
showsPrec :: Int -> SFactors a m -> ShowS
$cshowsPrec :: forall a (m :: Nat). Show a => Int -> SFactors a m -> ShowS
Show, (forall x. SFactors a m -> Rep (SFactors a m) x)
-> (forall x. Rep (SFactors a m) x -> SFactors a m)
-> Generic (SFactors a m)
forall x. Rep (SFactors a m) x -> SFactors a m
forall x. SFactors a m -> Rep (SFactors a m) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a (m :: Nat) x. Rep (SFactors a m) x -> SFactors a m
forall a (m :: Nat) x. SFactors a m -> Rep (SFactors a m) x
$cto :: forall a (m :: Nat) x. Rep (SFactors a m) x -> SFactors a m
$cfrom :: forall a (m :: Nat) x. SFactors a m -> Rep (SFactors a m) x
Generic)

instance Eq (SFactors a m) where
  SFactors a m
_ == :: SFactors a m -> SFactors a m -> Bool
== SFactors a m
_ = Bool
True

instance Ord (SFactors a m) where
  SFactors a m
_ compare :: SFactors a m -> SFactors a m -> Ordering
`compare` SFactors a m
_ = Ordering
EQ

instance NFData a => NFData (SFactors a m)

instance Ord a => Eq (Some (SFactors a)) where
  Some (SFactors [(Prime a, Word)]
xs) == :: Some (SFactors a) -> Some (SFactors a) -> Bool
== Some (SFactors [(Prime a, Word)]
ys) =
    [(Prime a, Word)]
xs [(Prime a, Word)] -> [(Prime a, Word)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(Prime a, Word)]
ys

instance Ord a => Ord (Some (SFactors a)) where
  Some (SFactors [(Prime a, Word)]
xs) compare :: Some (SFactors a) -> Some (SFactors a) -> Ordering
`compare` Some (SFactors [(Prime a, Word)]
ys) =
    [(Prime a, Word)]
xs [(Prime a, Word)] -> [(Prime a, Word)] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` [(Prime a, Word)]
ys

instance Show a => Show (Some (SFactors a)) where
  showsPrec :: Int -> Some (SFactors a) -> ShowS
showsPrec Int
p (Some SFactors a m
x) = Int -> SFactors a m -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p SFactors a m
x

instance NFData a => NFData (Some (SFactors a)) where
  rnf :: Some (SFactors a) -> ()
rnf (Some SFactors a m
x) = SFactors a m -> ()
forall a. NFData a => a -> ()
rnf SFactors a m
x

-- | Create a singleton from a type-level positive modulo @m@,
-- passed in a constraint.
--
-- >>> :set -XDataKinds
-- >>> sfactors :: SFactors Integer 13
-- SFactors {unSFactors = [(Prime 13,1)]}
sfactors :: forall a m. (Ord a, UniqueFactorisation a, KnownNat m) => SFactors a m
sfactors :: SFactors a m
sfactors = if a
m a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0
  then String -> SFactors a m
forall a. HasCallStack => String -> a
error String
"sfactors: modulo must be positive"
  else [(Prime a, Word)] -> SFactors a m
forall a (m :: Nat). [(Prime a, Word)] -> SFactors a m
SFactors ([(Prime a, Word)] -> [(Prime a, Word)]
forall a. Ord a => [a] -> [a]
sort (a -> [(Prime a, Word)]
forall a. UniqueFactorisation a => a -> [(Prime a, Word)]
factorise a
m))
  where
    m :: a
m = Natural -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy m -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy m
forall k (t :: k). Proxy t
Proxy :: Proxy m))

-- | Create a singleton from factors of @m@.
-- Factors must be distinct, as in output of 'factorise'.
--
-- >>> import Math.NumberTheory.Primes
-- >>> someSFactors (factorise 98)
-- SFactors {unSFactors = [(Prime 2,1),(Prime 7,2)]}
someSFactors :: (Ord a, Num a) => [(Prime a, Word)] -> Some (SFactors a)
someSFactors :: [(Prime a, Word)] -> Some (SFactors a)
someSFactors
  = SFactors a Any -> Some (SFactors a)
forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some
  (SFactors a Any -> Some (SFactors a))
-> ([(Prime a, Word)] -> SFactors a Any)
-> [(Prime a, Word)]
-> Some (SFactors a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Prime a, Word)] -> SFactors a Any
forall a (m :: Nat). [(Prime a, Word)] -> SFactors a m
SFactors
  -- Just a precaution against ill-formed lists of factors
  ([(Prime a, Word)] -> SFactors a Any)
-> ([(Prime a, Word)] -> [(Prime a, Word)])
-> [(Prime a, Word)]
-> SFactors a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Prime a) Word -> [(Prime a, Word)]
forall k a. Map k a -> [(k, a)]
M.assocs
  (Map (Prime a) Word -> [(Prime a, Word)])
-> ([(Prime a, Word)] -> Map (Prime a) Word)
-> [(Prime a, Word)]
-> [(Prime a, Word)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word -> Word -> Word) -> [(Prime a, Word)] -> Map (Prime a) Word
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith Word -> Word -> Word
forall a. Num a => a -> a -> a
(+)

-- | Convert a singleton to a proof that @m@ is known. Usage example:
--
-- > toModulo :: SFactors Integer m -> Natural
-- > toModulo t = case proofFromSFactors t of Sub Dict -> natVal t
proofFromSFactors :: Integral a => SFactors a m -> (() :- KnownNat m)
proofFromSFactors :: SFactors a m -> (() :: Constraint) :- KnownNat m
proofFromSFactors (SFactors [(Prime a, Word)]
fs) = ((() :: Constraint) => Dict (KnownNat m))
-> (() :: Constraint) :- KnownNat m
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((() :: Constraint) => Dict (KnownNat m))
 -> (() :: Constraint) :- KnownNat m)
-> ((() :: Constraint) => Dict (KnownNat m))
-> (() :: Constraint) :- KnownNat m
forall a b. (a -> b) -> a -> b
$ Magic Any -> Natural -> Dict (KnownNat m)
forall a b. a -> b
unsafeCoerce ((KnownNat Any => Dict (KnownNat Any)) -> Magic Any
forall (n :: Nat). (KnownNat n => Dict (KnownNat n)) -> Magic n
Magic KnownNat Any => Dict (KnownNat Any)
forall (a :: Constraint). a => Dict a
Dict) (a -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral' ([(Prime a, Word)] -> a
forall a. Num a => [(Prime a, Word)] -> a
factorBack [(Prime a, Word)]
fs) :: Natural)

-- | This singleton data type establishes a correspondence
-- between a modulo @m@ on type level
-- and a cyclic group of the same order on term level.
data CyclicGroup a (m :: Nat)
  = CG2' -- ^ Residues modulo 2.
  | CG4' -- ^ Residues modulo 4.
  | CGOddPrimePower'       (Prime a) Word
  -- ^ Residues modulo @p@^@k@ for __odd__ prime @p@.
  | CGDoubleOddPrimePower' (Prime a) Word
  -- ^ Residues modulo 2@p@^@k@ for __odd__ prime @p@.
  deriving (Int -> CyclicGroup a m -> ShowS
[CyclicGroup a m] -> ShowS
CyclicGroup a m -> String
(Int -> CyclicGroup a m -> ShowS)
-> (CyclicGroup a m -> String)
-> ([CyclicGroup a m] -> ShowS)
-> Show (CyclicGroup a m)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a (m :: Nat). Show a => Int -> CyclicGroup a m -> ShowS
forall a (m :: Nat). Show a => [CyclicGroup a m] -> ShowS
forall a (m :: Nat). Show a => CyclicGroup a m -> String
showList :: [CyclicGroup a m] -> ShowS
$cshowList :: forall a (m :: Nat). Show a => [CyclicGroup a m] -> ShowS
show :: CyclicGroup a m -> String
$cshow :: forall a (m :: Nat). Show a => CyclicGroup a m -> String
showsPrec :: Int -> CyclicGroup a m -> ShowS
$cshowsPrec :: forall a (m :: Nat). Show a => Int -> CyclicGroup a m -> ShowS
Show, (forall x. CyclicGroup a m -> Rep (CyclicGroup a m) x)
-> (forall x. Rep (CyclicGroup a m) x -> CyclicGroup a m)
-> Generic (CyclicGroup a m)
forall x. Rep (CyclicGroup a m) x -> CyclicGroup a m
forall x. CyclicGroup a m -> Rep (CyclicGroup a m) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a (m :: Nat) x. Rep (CyclicGroup a m) x -> CyclicGroup a m
forall a (m :: Nat) x. CyclicGroup a m -> Rep (CyclicGroup a m) x
$cto :: forall a (m :: Nat) x. Rep (CyclicGroup a m) x -> CyclicGroup a m
$cfrom :: forall a (m :: Nat) x. CyclicGroup a m -> Rep (CyclicGroup a m) x
Generic)

instance Eq (CyclicGroup a m) where
  CyclicGroup a m
_ == :: CyclicGroup a m -> CyclicGroup a m -> Bool
== CyclicGroup a m
_ = Bool
True

instance Ord (CyclicGroup a m) where
  CyclicGroup a m
_ compare :: CyclicGroup a m -> CyclicGroup a m -> Ordering
`compare` CyclicGroup a m
_ = Ordering
EQ

instance NFData a => NFData (CyclicGroup a m)

instance Eq a => Eq (Some (CyclicGroup a)) where
  Some CyclicGroup a m
CG2' == :: Some (CyclicGroup a) -> Some (CyclicGroup a) -> Bool
== Some CyclicGroup a m
CG2' = Bool
True
  Some CyclicGroup a m
CG4' == Some CyclicGroup a m
CG4' = Bool
True
  Some (CGOddPrimePower' Prime a
p1 Word
k1) == Some (CGOddPrimePower' Prime a
p2 Word
k2) =
    Prime a
p1 Prime a -> Prime a -> Bool
forall a. Eq a => a -> a -> Bool
== Prime a
p2 Bool -> Bool -> Bool
&& Word
k1 Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
k2
  Some (CGDoubleOddPrimePower' Prime a
p1 Word
k1) == Some (CGDoubleOddPrimePower' Prime a
p2 Word
k2) =
    Prime a
p1 Prime a -> Prime a -> Bool
forall a. Eq a => a -> a -> Bool
== Prime a
p2 Bool -> Bool -> Bool
&& Word
k1 Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
k2
  Some (CyclicGroup a)
_ == Some (CyclicGroup a)
_ = Bool
False

instance Ord a => Ord (Some (CyclicGroup a)) where
  compare :: Some (CyclicGroup a) -> Some (CyclicGroup a) -> Ordering
compare (Some CyclicGroup a m
x) (Some CyclicGroup a m
y) = case CyclicGroup a m
x of
    CyclicGroup a m
CG2' -> case CyclicGroup a m
y of
      CyclicGroup a m
CG2' -> Ordering
EQ
      CyclicGroup a m
_    -> Ordering
LT
    CyclicGroup a m
CG4' -> case CyclicGroup a m
y of
      CyclicGroup a m
CG2' -> Ordering
GT
      CyclicGroup a m
CG4' -> Ordering
EQ
      CyclicGroup a m
_    -> Ordering
LT
    CGOddPrimePower' Prime a
p1 Word
k1 -> case CyclicGroup a m
y of
      CGDoubleOddPrimePower'{} -> Ordering
LT
      CGOddPrimePower' Prime a
p2 Word
k2 ->
        Prime a
p1 Prime a -> Prime a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Prime a
p2 Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Word
k1 Word -> Word -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Word
k2
      CyclicGroup a m
_ -> Ordering
GT
    CGDoubleOddPrimePower' Prime a
p1 Word
k1 -> case CyclicGroup a m
y of
      CGDoubleOddPrimePower' Prime a
p2 Word
k2 ->
        Prime a
p1 Prime a -> Prime a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Prime a
p2 Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Word
k1 Word -> Word -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Word
k2
      CyclicGroup a m
_ -> Ordering
GT

instance Show a => Show (Some (CyclicGroup a)) where
  showsPrec :: Int -> Some (CyclicGroup a) -> ShowS
showsPrec Int
p (Some CyclicGroup a m
x) = Int -> CyclicGroup a m -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p CyclicGroup a m
x

instance NFData a => NFData (Some (CyclicGroup a)) where
  rnf :: Some (CyclicGroup a) -> ()
rnf (Some CyclicGroup a m
x) = CyclicGroup a m -> ()
forall a. NFData a => a -> ()
rnf CyclicGroup a m
x

-- | Create a singleton from a type-level positive modulo @m@,
-- passed in a constraint.
--
-- >>> :set -XDataKinds
-- >>> import Data.Maybe
-- >>> cyclicGroup :: Maybe (CyclicGroup Integer 169)
-- Just (CGOddPrimePower' (Prime 13) 2)
--
-- >>> :set -XTypeOperators -XNoStarIsType
-- >>> import GHC.TypeNats
-- >>> sfactorsToCyclicGroup (sfactors :: SFactors Integer 4)
-- Just CG4'
-- >>> sfactorsToCyclicGroup (sfactors :: SFactors Integer (2 * 13 ^ 3))
-- Just (CGDoubleOddPrimePower' (Prime 13) 3)
-- >>> sfactorsToCyclicGroup (sfactors :: SFactors Integer  (4 * 13))
-- Nothing
cyclicGroup
  :: forall a m.
     (Integral a, UniqueFactorisation a, KnownNat m)
  => Maybe (CyclicGroup a m)
cyclicGroup :: Maybe (CyclicGroup a m)
cyclicGroup = a -> Maybe (CyclicGroup a m)
forall a (m :: Nat).
(Integral a, UniqueFactorisation a) =>
a -> Maybe (CyclicGroup a m)
fromModuloInternal a
m
  where
    m :: a
m = Natural -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy m -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy m
forall k (t :: k). Proxy t
Proxy :: Proxy m))

-- | Create a singleton from factors.
-- Factors must be distinct, as in output of 'factorise'.
cyclicGroupFromFactors
  :: (Eq a, Num a)
  => [(Prime a, Word)]
  -> Maybe (Some (CyclicGroup a))
cyclicGroupFromFactors :: [(Prime a, Word)] -> Maybe (Some (CyclicGroup a))
cyclicGroupFromFactors = \case
  [(Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
1)] -> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a. a -> Maybe a
Just (Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a)))
-> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a b. (a -> b) -> a -> b
$ CyclicGroup a Any -> Some (CyclicGroup a)
forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some CyclicGroup a Any
forall a (m :: Nat). CyclicGroup a m
CG2'
  [(Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
2)] -> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a. a -> Maybe a
Just (Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a)))
-> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a b. (a -> b) -> a -> b
$ CyclicGroup a Any -> Some (CyclicGroup a)
forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some CyclicGroup a Any
forall a (m :: Nat). CyclicGroup a m
CG4'
  [(Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
_)] -> Maybe (Some (CyclicGroup a))
forall a. Maybe a
Nothing
  [(Prime a
p, Word
k)] -> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a. a -> Maybe a
Just (Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a)))
-> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a b. (a -> b) -> a -> b
$ CyclicGroup a Any -> Some (CyclicGroup a)
forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some (CyclicGroup a Any -> Some (CyclicGroup a))
-> CyclicGroup a Any -> Some (CyclicGroup a)
forall a b. (a -> b) -> a -> b
$ Prime a -> Word -> CyclicGroup a Any
forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGOddPrimePower' Prime a
p Word
k
  [(Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
1), (Prime a
p, Word
k)] -> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a. a -> Maybe a
Just (Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a)))
-> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a b. (a -> b) -> a -> b
$ CyclicGroup a Any -> Some (CyclicGroup a)
forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some (CyclicGroup a Any -> Some (CyclicGroup a))
-> CyclicGroup a Any -> Some (CyclicGroup a)
forall a b. (a -> b) -> a -> b
$ Prime a -> Word -> CyclicGroup a Any
forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' Prime a
p Word
k
  [(Prime a
p, Word
k), (Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
1)] -> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a. a -> Maybe a
Just (Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a)))
-> Some (CyclicGroup a) -> Maybe (Some (CyclicGroup a))
forall a b. (a -> b) -> a -> b
$ CyclicGroup a Any -> Some (CyclicGroup a)
forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some (CyclicGroup a Any -> Some (CyclicGroup a))
-> CyclicGroup a Any -> Some (CyclicGroup a)
forall a b. (a -> b) -> a -> b
$ Prime a -> Word -> CyclicGroup a Any
forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' Prime a
p Word
k
  [(Prime a, Word)]
_ -> Maybe (Some (CyclicGroup a))
forall a. Maybe a
Nothing

-- | Similar to 'cyclicGroupFromFactors' . 'factorise',
-- but much faster, because it
-- but performes only one primality test instead of full
-- factorisation.
cyclicGroupFromModulo
  :: (Integral a, UniqueFactorisation a)
  => a
  -> Maybe (Some (CyclicGroup a))
cyclicGroupFromModulo :: a -> Maybe (Some (CyclicGroup a))
cyclicGroupFromModulo = (CyclicGroup a Any -> Some (CyclicGroup a))
-> Maybe (CyclicGroup a Any) -> Maybe (Some (CyclicGroup a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CyclicGroup a Any -> Some (CyclicGroup a)
forall (a :: Nat -> *) (m :: Nat). a m -> Some a
Some (Maybe (CyclicGroup a Any) -> Maybe (Some (CyclicGroup a)))
-> (a -> Maybe (CyclicGroup a Any))
-> a
-> Maybe (Some (CyclicGroup a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe (CyclicGroup a Any)
forall a (m :: Nat).
(Integral a, UniqueFactorisation a) =>
a -> Maybe (CyclicGroup a m)
fromModuloInternal

fromModuloInternal
  :: (Integral a, UniqueFactorisation a)
  => a
  -> Maybe (CyclicGroup a m)
fromModuloInternal :: a -> Maybe (CyclicGroup a m)
fromModuloInternal = \case
  a
2 -> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a. a -> Maybe a
Just CyclicGroup a m
forall a (m :: Nat). CyclicGroup a m
CG2'
  a
4 -> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a. a -> Maybe a
Just CyclicGroup a m
forall a (m :: Nat). CyclicGroup a m
CG4'
  a
n
    | a -> Bool
forall a. Integral a => a -> Bool
even a
n -> (Prime a -> Word -> CyclicGroup a m)
-> (Prime a, Word) -> CyclicGroup a m
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Prime a -> Word -> CyclicGroup a m
forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' ((Prime a, Word) -> CyclicGroup a m)
-> Maybe (Prime a, Word) -> Maybe (CyclicGroup a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe (Prime a, Word)
forall a.
(Integral a, UniqueFactorisation a) =>
a -> Maybe (Prime a, Word)
isOddPrimePower (a
n a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
2)
    | Bool
otherwise -> (Prime a -> Word -> CyclicGroup a m)
-> (Prime a, Word) -> CyclicGroup a m
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Prime a -> Word -> CyclicGroup a m
forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGOddPrimePower' ((Prime a, Word) -> CyclicGroup a m)
-> Maybe (Prime a, Word) -> Maybe (CyclicGroup a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe (Prime a, Word)
forall a.
(Integral a, UniqueFactorisation a) =>
a -> Maybe (Prime a, Word)
isOddPrimePower a
n

isOddPrimePower
  :: (Integral a, UniqueFactorisation a)
  => a
  -> Maybe (Prime a, Word)
isOddPrimePower :: a -> Maybe (Prime a, Word)
isOddPrimePower a
n
  | a -> Bool
forall a. Integral a => a -> Bool
even a
n    = Maybe (Prime a, Word)
forall a. Maybe a
Nothing
  | Bool
otherwise = (, Word
k) (Prime a -> (Prime a, Word))
-> Maybe (Prime a) -> Maybe (Prime a, Word)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe (Prime a)
forall a. UniqueFactorisation a => a -> Maybe (Prime a)
isPrime a
p
  where
    (a
p, Word
k) = a -> (a, Word)
forall a. Integral a => a -> (a, Word)
highestPower a
n

-- | Convert a cyclic group to a proof that @m@ is known. Usage example:
--
-- > toModulo :: CyclicGroup Integer m -> Natural
-- > toModulo t = case proofFromCyclicGroup t of Sub Dict -> natVal t
proofFromCyclicGroup :: Integral a => CyclicGroup a m -> (() :- KnownNat m)
proofFromCyclicGroup :: CyclicGroup a m -> (() :: Constraint) :- KnownNat m
proofFromCyclicGroup = SFactors a m -> (() :: Constraint) :- KnownNat m
forall a (m :: Nat).
Integral a =>
SFactors a m -> (() :: Constraint) :- KnownNat m
proofFromSFactors (SFactors a m -> (() :: Constraint) :- KnownNat m)
-> (CyclicGroup a m -> SFactors a m)
-> CyclicGroup a m
-> (() :: Constraint) :- KnownNat m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CyclicGroup a m -> SFactors a m
forall a (m :: Nat). Num a => CyclicGroup a m -> SFactors a m
cyclicGroupToSFactors

-- | Check whether a multiplicative group of residues,
-- characterized by its modulo, is cyclic and, if yes, return its form.
--
-- >>> :set -XTypeOperators -XNoStarIsType
-- >>> import GHC.TypeNats
-- >>> sfactorsToCyclicGroup (sfactors :: SFactors Integer 4)
-- Just CG4'
-- >>> sfactorsToCyclicGroup (sfactors :: SFactors Integer (2 * 13 ^ 3))
-- Just (CGDoubleOddPrimePower' (Prime 13) 3)
-- >>> sfactorsToCyclicGroup (sfactors :: SFactors Integer  (4 * 13))
-- Nothing
sfactorsToCyclicGroup :: (Eq a, Num a) => SFactors a m -> Maybe (CyclicGroup a m)
sfactorsToCyclicGroup :: SFactors a m -> Maybe (CyclicGroup a m)
sfactorsToCyclicGroup (SFactors [(Prime a, Word)]
fs) = case [(Prime a, Word)]
fs of
  [(Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
1)]         -> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a. a -> Maybe a
Just CyclicGroup a m
forall a (m :: Nat). CyclicGroup a m
CG2'
  [(Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
2)]         -> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a. a -> Maybe a
Just CyclicGroup a m
forall a (m :: Nat). CyclicGroup a m
CG4'
  [(Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
_)]         -> Maybe (CyclicGroup a m)
forall a. Maybe a
Nothing
  [(Prime a
p, Word
k)]                    -> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a. a -> Maybe a
Just (CyclicGroup a m -> Maybe (CyclicGroup a m))
-> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a b. (a -> b) -> a -> b
$ Prime a -> Word -> CyclicGroup a m
forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGOddPrimePower' Prime a
p Word
k
  [(Prime a
p, Word
k), (Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
1)] -> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a. a -> Maybe a
Just (CyclicGroup a m -> Maybe (CyclicGroup a m))
-> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a b. (a -> b) -> a -> b
$ Prime a -> Word -> CyclicGroup a m
forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' Prime a
p Word
k
  [(Prime a -> a
forall a. Prime a -> a
unPrime -> a
2, Word
1), (Prime a
p, Word
k)] -> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a. a -> Maybe a
Just (CyclicGroup a m -> Maybe (CyclicGroup a m))
-> CyclicGroup a m -> Maybe (CyclicGroup a m)
forall a b. (a -> b) -> a -> b
$ Prime a -> Word -> CyclicGroup a m
forall a (m :: Nat). Prime a -> Word -> CyclicGroup a m
CGDoubleOddPrimePower' Prime a
p Word
k
  [(Prime a, Word)]
_ -> Maybe (CyclicGroup a m)
forall a. Maybe a
Nothing

-- | Invert 'sfactorsToCyclicGroup'.
--
-- >>> import Data.Maybe
-- >>> cyclicGroupToSFactors (fromJust (sfactorsToCyclicGroup (sfactors :: SFactors Integer 4)))
-- SFactors {unSFactors = [(Prime 2,2)]}
cyclicGroupToSFactors :: Num a => CyclicGroup a m -> SFactors a m
cyclicGroupToSFactors :: CyclicGroup a m -> SFactors a m
cyclicGroupToSFactors = [(Prime a, Word)] -> SFactors a m
forall a (m :: Nat). [(Prime a, Word)] -> SFactors a m
SFactors ([(Prime a, Word)] -> SFactors a m)
-> (CyclicGroup a m -> [(Prime a, Word)])
-> CyclicGroup a m
-> SFactors a m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
  CyclicGroup a m
CG2' -> [(a -> Prime a
forall a. a -> Prime a
Prime a
2, Word
1)]
  CyclicGroup a m
CG4' -> [(a -> Prime a
forall a. a -> Prime a
Prime a
2, Word
2)]
  CGOddPrimePower' Prime a
p Word
k -> [(Prime a
p, Word
k)]
  CGDoubleOddPrimePower' Prime a
p Word
k -> [(a -> Prime a
forall a. a -> Prime a
Prime a
2, Word
1), (Prime a
p, Word
k)]

-- | Unidirectional pattern for residues modulo 2.
pattern CG2 :: CyclicGroup a m
pattern $mCG2 :: forall r a (m :: Nat).
CyclicGroup a m -> (Void# -> r) -> (Void# -> r) -> r
CG2 <- CG2'

-- | Unidirectional pattern for residues modulo 4.
pattern CG4 :: CyclicGroup a m
pattern $mCG4 :: forall r a (m :: Nat).
CyclicGroup a m -> (Void# -> r) -> (Void# -> r) -> r
CG4 <- CG4'

-- | Unidirectional pattern for residues modulo @p@^@k@ for __odd__ prime @p@.
pattern CGOddPrimePower :: Prime a -> Word -> CyclicGroup a m
pattern $mCGOddPrimePower :: forall r a (m :: Nat).
CyclicGroup a m -> (Prime a -> Word -> r) -> (Void# -> r) -> r
CGOddPrimePower p k <- CGOddPrimePower' p k

-- | Unidirectional pattern for residues modulo 2@p@^@k@ for __odd__ prime @p@.
pattern CGDoubleOddPrimePower :: Prime a -> Word -> CyclicGroup a m
pattern $mCGDoubleOddPrimePower :: forall r a (m :: Nat).
CyclicGroup a m -> (Prime a -> Word -> r) -> (Void# -> r) -> r
CGDoubleOddPrimePower p k <- CGDoubleOddPrimePower' p k

#if __GLASGOW_HASKELL__ > 801
{-# COMPLETE CG2, CG4, CGOddPrimePower, CGDoubleOddPrimePower #-}
#endif