{-# 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
, sfactors
, someSFactors
, unSFactors
, proofFromSFactors
, CyclicGroup
, cyclicGroup
, cyclicGroupFromFactors
, cyclicGroupFromModulo
, proofFromCyclicGroup
, pattern CG2
, pattern CG4
, pattern CGOddPrimePower
, pattern CGDoubleOddPrimePower
, cyclicGroupToSFactors
, sfactorsToCyclicGroup
, 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
data Some (a :: Nat -> Type) where
Some :: a m -> Some a
newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
newtype SFactors a (m :: Nat) = SFactors
{ SFactors a m -> [(Prime a, Word)]
unSFactors :: [(Prime a, Word)]
} 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
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))
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
([(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
(+)
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)
data CyclicGroup a (m :: Nat)
= CG2'
| CG4'
| CGOddPrimePower' (Prime a) Word
| CGDoubleOddPrimePower' (Prime a) Word
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
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))
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
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
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
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
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)]
pattern CG2 :: CyclicGroup a m
pattern $mCG2 :: forall r a (m :: Nat).
CyclicGroup a m -> (Void# -> r) -> (Void# -> r) -> r
CG2 <- CG2'
pattern CG4 :: CyclicGroup a m
pattern $mCG4 :: forall r a (m :: Nat).
CyclicGroup a m -> (Void# -> r) -> (Void# -> r) -> r
CG4 <- CG4'
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
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