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

    {-# 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
    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
      { forall a (m :: Nat). 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
    $cshowsPrec :: forall a (m :: Nat). Show a => Int -> SFactors a m -> ShowS
    showsPrec :: Int -> SFactors a m -> ShowS
    $cshow :: forall a (m :: Nat). Show a => SFactors a m -> String
    show :: SFactors a m -> String
    $cshowList :: forall a (m :: Nat). Show a => [SFactors a m] -> ShowS
    showList :: [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
    $cfrom :: forall a (m :: Nat) x. SFactors a m -> Rep (SFactors a m) x
    from :: forall x. SFactors a m -> Rep (SFactors a m) x
    $cto :: forall a (m :: Nat) x. Rep (SFactors a m) x -> SFactors a m
    to :: forall x. Rep (SFactors a m) x -> SFactors a m
    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 :: forall a (m :: Nat).
    (Ord a, UniqueFactorisation a, KnownNat m) =>
    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 = Nat -> a
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Proxy m -> Nat
    forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
    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 :: forall a. (Ord a, Num a) => [(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 :: forall a (m :: Nat).
    Integral a =>
    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 -> Nat -> 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 Dict (KnownNat Any)
    KnownNat Any => Dict (KnownNat Any)
    forall (a :: Constraint). a => Dict a
    Dict) (a -> Nat
    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
    $cshowsPrec :: forall a (m :: Nat). Show a => Int -> CyclicGroup a m -> ShowS
    showsPrec :: Int -> CyclicGroup a m -> ShowS
    $cshow :: forall a (m :: Nat). Show a => CyclicGroup a m -> String
    show :: CyclicGroup a m -> String
    $cshowList :: forall a (m :: Nat). Show a => [CyclicGroup a m] -> ShowS
    showList :: [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
    $cfrom :: forall a (m :: Nat) x. CyclicGroup a m -> Rep (CyclicGroup a m) x
    from :: forall x. CyclicGroup a m -> Rep (CyclicGroup a m) x
    $cto :: forall a (m :: Nat) x. Rep (CyclicGroup a m) x -> CyclicGroup a m
    to :: forall x. Rep (CyclicGroup a m) x -> CyclicGroup a m
    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 :: forall a (m :: Nat).
    (Integral a, UniqueFactorisation a, KnownNat m) =>
    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 = Nat -> a
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Proxy m -> Nat
    forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
    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 :: forall a.
    (Eq a, Num a) =>
    [(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 :: forall a.
    (Integral a, UniqueFactorisation a) =>
    a -> Maybe (Some (CyclicGroup a))
    cyclicGroupFromModulo = (CyclicGroup a Any -> Some (CyclicGroup a))
    -> Maybe (CyclicGroup a Any) -> Maybe (Some (CyclicGroup a))
    forall a b. (a -> b) -> Maybe a -> Maybe b
    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 :: forall a (m :: Nat).
    (Integral a, UniqueFactorisation a) =>
    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 :: forall a.
    (Integral a, UniqueFactorisation a) =>
    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 :: forall a (m :: Nat).
    Integral a =>
    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 :: forall a (m :: Nat).
    (Eq a, Num a) =>
    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 :: forall a (m :: Nat). Num a => 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 -> ((# #) -> r) -> ((# #) -> 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 -> ((# #) -> r) -> ((# #) -> 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) -> ((# #) -> 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) -> ((# #) -> r) -> r
    CGDoubleOddPrimePower p k <- CGDoubleOddPrimePower' p k

    {-# COMPLETE CG2, CG4, CGOddPrimePower, CGDoubleOddPrimePower #-}