{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}

module Algebra.Field.Galois
  ( GF' (),
    IsGF',
    modPoly,
    modVec,
    withIrreducible,
    linearRepGF,
    linearRepGF',
    reifyGF',
    generateIrreducible,
    withGF',
    GF,
    ConwayPolynomial (..),
    Conway,
    primitive,
    primitive',
    conway,
    conwayFile,
    addConwayPolynomials,
  )
where

import Algebra.Field.Galois.Conway
import Algebra.Field.Prime
import Algebra.Internal
import Algebra.Prelude.Core hiding (varX)
import Algebra.Ring.Polynomial.Univariate
import Control.DeepSeq
import Control.Lens (imap)
import Control.Monad.Loops (iterateUntil)
import Control.Monad.Random (MonadRandom, Random (..), getRandom, getRandomR, runRand)
import qualified Data.Foldable as F
import Data.Kind (Type)
import qualified Data.Ratio as Rat
import Data.Reflection (Reifies (..), reify)
import qualified Data.Sized as SV
import qualified Data.Traversable as T
import qualified Data.Vector as V
import qualified GHC.TypeLits as TL
import qualified Numeric.Algebra as NA
import qualified Prelude as P

{- | Galois field of order @p^n@.
   @f@ stands for the irreducible polynomial over @F_p@ of degree @n@.
-}
newtype GF' p (n :: TL.Nat) (f :: Type) = GF' {GF' p n f -> Sized n (F p)
runGF' :: Sized n (F p)}
  deriving newtype (GF' p n f -> ()
(GF' p n f -> ()) -> NFData (GF' p n f)
forall a. (a -> ()) -> NFData a
forall k (p :: k) (n :: Nat) f. GF' p n f -> ()
rnf :: GF' p n f -> ()
$crnf :: forall k (p :: k) (n :: Nat) f. GF' p n f -> ()
NFData)

deriving instance Reifies p Integer => Eq (GF' p n f)

{- | Galois Field of order @p^n@. This uses conway polynomials
   as canonical minimal polynomial and it should be known at
   compile-time (i.e. @Reifies (Conway p n) (Unipol (F n))@
   instances should be defined to use field operations).
-}
type GF (p :: TL.Nat) n = GF' p n (Conway p n)

modPoly :: forall p n f. (KnownNat n, Reifies p Integer) => Unipol (F p) -> GF' p n f
modPoly :: Unipol (F p) -> GF' p n f
modPoly = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f)
-> (Unipol (F p) -> Sized n (F p)) -> Unipol (F p) -> GF' p n f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unipol (F p) -> Sized n (F p)
forall (n :: Nat) r.
(CoeffRing r, KnownNat n) =>
Unipol r -> Sized n r
polyToVec

modVec :: Sized n (F p) -> GF' p n f
modVec :: Sized n (F p) -> GF' p n f
modVec = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF'

instance (Reifies p Integer, KnownNat n, Show (F p)) => Show (GF' p n f) where
  showsPrec :: Int -> GF' p n f -> ShowS
showsPrec Int
d (GF' (F p
v :< Sized Vector n1 (F p)
vs)) =
    if (F p -> Bool) -> Sized Vector n1 (F p) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
F.all F p -> Bool
forall r. DecidableZero r => r -> Bool
isZero Sized Vector n1 (F p)
vs
      then Int -> F p -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d F p
v
      else Char -> ShowS
showChar Char
'<' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString (Sized (Arity (Unipol (F p))) String
-> Int -> Unipol (F p) -> String
forall poly.
(IsOrderedPolynomial poly, PrettyCoeff (Coefficient poly)) =>
Sized (Arity poly) String -> Int -> poly -> String
showPolynomialWith (String -> Sized Vector 1 String
forall (f :: * -> *) a. (CPointed f, Dom f a) => a -> Sized f 1 a
singleton String
"ξ") Int
0 (Unipol (F p) -> String) -> Unipol (F p) -> String
forall a b. (a -> b) -> a -> b
$ Sized Vector n (F p) -> Unipol (F p)
forall r (n :: Nat). CoeffRing r => Sized n r -> Unipol r
vecToPoly (Sized Vector n (F p) -> Unipol (F p))
-> Sized Vector n (F p) -> Unipol (F p)
forall a b. (a -> b) -> a -> b
$ F p
v F p -> Sized Vector n1 (F p) -> Sized Vector n (F p)
forall (f :: * -> *) a (n :: Nat) (n1 :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f, n ~ (1 + n1), KnownNat n1) =>
a -> Sized f n1 a -> Sized f n a
:< Sized Vector n1 (F p)
vs) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
'>'
  showsPrec Int
_ GF' p n f
_ = String -> ShowS
showString String
"0"

instance (Reifies p Integer, KnownNat n, Show (F p)) => PrettyCoeff (GF' p n f)

varX :: CoeffRing r => Unipol r
varX :: Unipol r
varX = Ordinal (Arity (Unipol r)) -> Unipol r
forall poly. IsPolynomial poly => Ordinal (Arity poly) -> poly
var [od|0|]

vecToPoly ::
  (CoeffRing r) =>
  Sized n r ->
  Unipol r
vecToPoly :: Sized n r -> Unipol r
vecToPoly Sized n r
v = [Unipol r] -> Unipol r
forall (f :: * -> *) m. (Foldable f, Monoidal m) => f m -> m
sum ([Unipol r] -> Unipol r) -> [Unipol r] -> Unipol r
forall a b. (a -> b) -> a -> b
$ (Int -> r -> Unipol r) -> [r] -> [Unipol r]
forall i (f :: * -> *) a b.
FunctorWithIndex i f =>
(i -> a -> b) -> f a -> f b
imap (\Int
i r
c -> Coefficient (Unipol r) -> Unipol r
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff r
Coefficient (Unipol r)
c Unipol r -> Unipol r -> Unipol r
forall r. Multiplicative r => r -> r -> r
* Unipol r
forall r. CoeffRing r => Unipol r
varX Unipol r -> Natural -> Unipol r
forall r. Unital r => r -> Natural -> r
^ Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i) ([r] -> [Unipol r]) -> [r] -> [Unipol r]
forall a b. (a -> b) -> a -> b
$ Sized n r -> [r]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Sized n r
v

polyToVec :: forall n r. (CoeffRing r, KnownNat n) => Unipol r -> Sized n r
polyToVec :: Unipol r -> Sized n r
polyToVec Unipol r
f =
  case SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n) of
    ZeroOrSucc n
IsZero -> Sized n r
forall (f :: * -> *) a. (Monoid (f a), Dom f a) => Sized f 0 a
SV.empty
    IsSucc SNat n1
_ ->
      [r] -> Sized n r
forall (f :: * -> *) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
[a] -> Sized f n a
unsafeFromList'
        [ OrderedMonomial (MOrder (Unipol r)) (Arity (Unipol r))
-> Unipol r -> Coefficient (Unipol r)
forall poly.
IsOrderedPolynomial poly =>
OrderedMonomial (MOrder poly) (Arity poly)
-> poly -> Coefficient poly
coeff (Monomial 1 -> OrderedMonomial Grevlex 1
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial 1 -> OrderedMonomial Grevlex 1)
-> Monomial 1 -> OrderedMonomial Grevlex 1
forall a b. (a -> b) -> a -> b
$ Int -> Monomial 1
forall (f :: * -> *) a. (CPointed f, Dom f a) => a -> Sized f 1 a
SV.singleton Int
i) Unipol r
f
        | Int
i <- [Int
0 .. Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n)) Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
1]
        ]

instance Reifies p Integer => Additive (GF' p n f) where
  GF' Sized n (F p)
v + :: GF' p n f -> GF' p n f -> GF' p n f
+ GF' Sized n (F p)
u = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ (F p -> F p -> F p)
-> Sized n (F p) -> Sized n (F p) -> Sized n (F p)
forall (f :: * -> *) (n :: Nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
SV.zipWithSame F p -> F p -> F p
forall r. Additive r => r -> r -> r
(+) Sized n (F p)
v Sized n (F p)
u

instance (Reifies p Integer, KnownNat n) => Monoidal (GF' p n f) where
  zero :: GF' p n f
zero = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ F p -> Sized n (F p)
forall (f :: * -> *) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
SV.replicate' F p
forall m. Monoidal m => m
zero

instance Reifies p Integer => LeftModule Natural (GF' p n f) where
  Natural
n .* :: Natural -> GF' p n f -> GF' p n f
.* GF' Sized n (F p)
v = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ (F p -> F p) -> Sized n (F p) -> Sized n (F p)
forall (f :: * -> *) (n :: Nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) -> Sized f n a -> Sized f n b
SV.map (Natural
n Natural -> F p -> F p
forall r m. LeftModule r m => r -> m -> m
.*) Sized n (F p)
v

instance Reifies p Integer => RightModule Natural (GF' p n f) where
  GF' Sized n (F p)
v *. :: GF' p n f -> Natural -> GF' p n f
*. Natural
n = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ (F p -> F p) -> Sized n (F p) -> Sized n (F p)
forall (f :: * -> *) (n :: Nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) -> Sized f n a -> Sized f n b
SV.map (F p -> Natural -> F p
forall r m. RightModule r m => m -> r -> m
*. Natural
n) Sized n (F p)
v

instance Reifies p Integer => LeftModule Integer (GF' p n f) where
  Integer
n .* :: Integer -> GF' p n f -> GF' p n f
.* GF' Sized n (F p)
v = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ (F p -> F p) -> Sized n (F p) -> Sized n (F p)
forall (f :: * -> *) (n :: Nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) -> Sized f n a -> Sized f n b
SV.map (Integer
n Integer -> F p -> F p
forall r m. LeftModule r m => r -> m -> m
.*) Sized n (F p)
v

instance Reifies p Integer => RightModule Integer (GF' p n f) where
  GF' Sized n (F p)
v *. :: GF' p n f -> Integer -> GF' p n f
*. Integer
n = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ (F p -> F p) -> Sized n (F p) -> Sized n (F p)
forall (f :: * -> *) (n :: Nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) -> Sized f n a -> Sized f n b
SV.map (F p -> Integer -> F p
forall r m. RightModule r m => m -> r -> m
*. Integer
n) Sized n (F p)
v

instance (KnownNat n, Reifies p Integer) => Group (GF' p n f) where
  negate :: GF' p n f -> GF' p n f
negate (GF' Sized n (F p)
v) = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ (F p -> F p) -> Sized n (F p) -> Sized n (F p)
forall (f :: * -> *) (n :: Nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) -> Sized f n a -> Sized f n b
SV.map F p -> F p
forall r. Group r => r -> r
negate Sized n (F p)
v
  GF' Sized n (F p)
u - :: GF' p n f -> GF' p n f -> GF' p n f
- GF' Sized n (F p)
v = Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ (F p -> F p -> F p)
-> Sized n (F p) -> Sized n (F p) -> Sized n (F p)
forall (f :: * -> *) (n :: Nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
SV.zipWithSame (-) Sized n (F p)
u Sized n (F p)
v

instance (Reifies p Integer) => Abelian (GF' p n f)

instance
  (KnownNat n, Reifies f (Unipol (F p)), Reifies p Integer) =>
  Multiplicative (GF' p n f)
  where
  GF' Sized n (F p)
u * :: GF' p n f -> GF' p n f -> GF' p n f
* GF' Sized n (F p)
v =
    let t :: Unipol (F p)
t = (Sized n (F p) -> Unipol (F p)
forall r (n :: Nat). CoeffRing r => Sized n r -> Unipol r
vecToPoly Sized n (F p)
u Unipol (F p) -> Unipol (F p) -> Unipol (F p)
forall r. Multiplicative r => r -> r -> r
* Sized n (F p) -> Unipol (F p)
forall r (n :: Nat). CoeffRing r => Sized n r -> Unipol r
vecToPoly Sized n (F p)
v) Unipol (F p) -> Unipol (F p) -> Unipol (F p)
forall d. Euclidean d => d -> d -> d
`rem` Proxy f -> Unipol (F p)
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy f
forall k (t :: k). Proxy t
Proxy :: Proxy f)
     in Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ Unipol (F p) -> Sized n (F p)
forall (n :: Nat) r.
(CoeffRing r, KnownNat n) =>
Unipol r -> Sized n r
polyToVec Unipol (F p)
t

instance (KnownNat n, Reifies f (Unipol (F p)), Reifies p Integer) => Unital (GF' p n f) where
  one :: GF' p n f
one =
    case SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n) of
      ZeroOrSucc n
IsZero -> Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' Sized n (F p)
forall (f :: * -> *) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, n ~ 0) =>
Sized f n a
Nil
      IsSucc SNat n1
k ->
        SNat n1 -> (KnownNat n1 => GF' p n f) -> GF' p n f
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
k ((KnownNat n1 => GF' p n f) -> GF' p n f)
-> (KnownNat n1 => GF' p n f) -> GF' p n f
forall a b. (a -> b) -> a -> b
$
          Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$
            F p
forall r. Unital r => r
one F p -> Sized Vector n1 (F p) -> Sized n (F p)
forall (f :: * -> *) a (n :: Nat) (n1 :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f, n ~ (1 + n1), KnownNat n1) =>
a -> Sized f n1 a -> Sized f n a
:< SNat n1 -> F p -> Sized Vector n1 (F p)
forall (f :: * -> *) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
SV.replicate SNat n1
k F p
forall m. Monoidal m => m
zero

instance (KnownNat n, Reifies f (Unipol (F p)), Reifies p Integer) => Semiring (GF' p n f)

instance (KnownNat n, Reifies f (Unipol (F p)), Reifies p Integer) => Rig (GF' p n f) where
  fromNatural :: Natural -> GF' p n f
fromNatural Natural
n =
    case SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n) of
      ZeroOrSucc n
IsZero -> Sized 0 (F p) -> GF' p 0 f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' Sized 0 (F p)
forall (f :: * -> *) a. (Monoid (f a), Dom f a) => Sized f 0 a
SV.empty
      IsSucc SNat n1
k ->
        SNat n1 -> (KnownNat n1 => GF' p n f) -> GF' p n f
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
k ((KnownNat n1 => GF' p n f) -> GF' p n f)
-> (KnownNat n1 => GF' p n f) -> GF' p n f
forall a b. (a -> b) -> a -> b
$
          Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$
            Natural -> F p
forall r. Rig r => Natural -> r
fromNatural Natural
n F p -> Sized Vector n1 (F p) -> Sized n (F p)
forall (f :: * -> *) a (n :: Nat) (n1 :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f, n ~ (1 + n1), KnownNat n1) =>
a -> Sized f n1 a -> Sized f n a
:< SNat n1 -> F p -> Sized Vector n1 (F p)
forall (f :: * -> *) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
SV.replicate SNat n1
k F p
forall m. Monoidal m => m
zero

instance (KnownNat n, Reifies f (Unipol (F p)), Reifies p Integer) => Commutative (GF' p n f)

instance (KnownNat n, Reifies f (Unipol (F p)), Reifies p Integer) => Ring (GF' p n f) where
  fromInteger :: Integer -> GF' p n f
fromInteger Integer
n =
    case SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n) of
      ZeroOrSucc n
IsZero -> Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' Sized n (F p)
forall (f :: * -> *) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, n ~ 0) =>
Sized f n a
Nil
      IsSucc SNat n1
k ->
        SNat n1 -> (KnownNat n1 => GF' p n f) -> GF' p n f
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
k ((KnownNat n1 => GF' p n f) -> GF' p n f)
-> (KnownNat n1 => GF' p n f) -> GF' p n f
forall a b. (a -> b) -> a -> b
$
          Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ Integer -> F p
forall r. Num r => Integer -> r
fromInteger Integer
n F p -> Sized Vector n1 (F p) -> Sized n (F p)
forall (f :: * -> *) a (n :: Nat) (n1 :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f, n ~ (1 + n1), KnownNat n1) =>
a -> Sized f n1 a -> Sized f n a
:< SNat n1 -> F p -> Sized Vector n1 (F p)
forall (f :: * -> *) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
SV.replicate SNat n1
k F p
forall m. Monoidal m => m
zero

instance (KnownNat n, Reifies p Integer) => DecidableZero (GF' p n f) where
  isZero :: GF' p n f -> Bool
isZero (GF' Sized n (F p)
sv) = (F p -> Bool) -> Sized n (F p) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
F.all F p -> Bool
forall r. DecidableZero r => r -> Bool
isZero Sized n (F p)
sv

instance (KnownNat n, Reifies p Integer, Reifies f (Unipol (F p))) => DecidableUnits (GF' p n f) where
  isUnit :: GF' p n f -> Bool
isUnit (GF' Sized n (F p)
sv) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (F p -> Bool) -> Sized n (F p) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
F.all F p -> Bool
forall r. DecidableZero r => r -> Bool
isZero Sized n (F p)
sv
  recipUnit :: GF' p n f -> Maybe (GF' p n f)
recipUnit GF' p n f
a
    | GF' p n f -> Bool
forall r. DecidableZero r => r -> Bool
isZero GF' p n f
a = Maybe (GF' p n f)
forall a. Maybe a
Nothing
    | Bool
otherwise = GF' p n f -> Maybe (GF' p n f)
forall a. a -> Maybe a
Just (GF' p n f -> Maybe (GF' p n f)) -> GF' p n f -> Maybe (GF' p n f)
forall a b. (a -> b) -> a -> b
$ GF' p n f -> GF' p n f
forall r. Division r => r -> r
recip GF' p n f
a

instance
  (Reifies p Integer, Reifies f (Unipol (F p)), KnownNat n) =>
  Characteristic (GF' p n f)
  where
  char :: proxy (GF' p n f) -> Natural
char proxy (GF' p n f)
_ = Proxy (F p) -> Natural
forall r (proxy :: * -> *). Characteristic r => proxy r -> Natural
char (Proxy (F p)
forall k (t :: k). Proxy t
Proxy :: Proxy (F p))

instance
  (Reifies p Integer, Reifies f (Unipol (F p)), KnownNat n) =>
  Division (GF' p n f)
  where
  recip :: GF' p n f -> GF' p n f
recip GF' p n f
f =
    let p :: Unipol (F p)
p = Proxy f -> Unipol (F p)
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy f
forall k (t :: k). Proxy t
Proxy :: Proxy f)
        (Unipol (F p)
_, Unipol (F p)
_, Unipol (F p)
r) = [(Unipol (F p), Unipol (F p), Unipol (F p))]
-> (Unipol (F p), Unipol (F p), Unipol (F p))
forall a. [a] -> a
P.head ([(Unipol (F p), Unipol (F p), Unipol (F p))]
 -> (Unipol (F p), Unipol (F p), Unipol (F p)))
-> [(Unipol (F p), Unipol (F p), Unipol (F p))]
-> (Unipol (F p), Unipol (F p), Unipol (F p))
forall a b. (a -> b) -> a -> b
$ Unipol (F p)
-> Unipol (F p) -> [(Unipol (F p), Unipol (F p), Unipol (F p))]
forall d. Euclidean d => d -> d -> [(d, d, d)]
euclid Unipol (F p)
p (Unipol (F p) -> [(Unipol (F p), Unipol (F p), Unipol (F p))])
-> Unipol (F p) -> [(Unipol (F p), Unipol (F p), Unipol (F p))]
forall a b. (a -> b) -> a -> b
$ Sized n (F p) -> Unipol (F p)
forall r (n :: Nat). CoeffRing r => Sized n r -> Unipol r
vecToPoly (Sized n (F p) -> Unipol (F p)) -> Sized n (F p) -> Unipol (F p)
forall a b. (a -> b) -> a -> b
$ GF' p n f -> Sized n (F p)
forall k (p :: k) (n :: Nat) f. GF' p n f -> Sized n (F p)
runGF' GF' p n f
f
     in Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ Unipol (F p) -> Sized n (F p)
forall (n :: Nat) r.
(CoeffRing r, KnownNat n) =>
Unipol r -> Sized n r
polyToVec (Unipol (F p) -> Sized n (F p)) -> Unipol (F p) -> Sized n (F p)
forall a b. (a -> b) -> a -> b
$ Unipol (F p)
r Unipol (F p) -> Unipol (F p) -> Unipol (F p)
forall d. Euclidean d => d -> d -> d
`rem` Unipol (F p)
p

instance
  (KnownNat n, Reifies p Integer, Reifies f (Unipol (F p))) =>
  DecidableAssociates (GF' p n f)
  where
  isAssociate :: GF' p n f -> GF' p n f -> Bool
isAssociate GF' p n f
p GF' p n f
n =
    (GF' p n f -> Bool
forall r. DecidableZero r => r -> Bool
isZero GF' p n f
p Bool -> Bool -> Bool
&& GF' p n f -> Bool
forall r. DecidableZero r => r -> Bool
isZero GF' p n f
n) Bool -> Bool -> Bool
|| (Bool -> Bool
not (GF' p n f -> Bool
forall r. DecidableZero r => r -> Bool
isZero GF' p n f
p) Bool -> Bool -> Bool
&& Bool -> Bool
not (GF' p n f -> Bool
forall r. DecidableZero r => r -> Bool
isZero GF' p n f
n))

instance
  (KnownNat n, Reifies p Integer, Reifies f (Unipol (F p))) =>
  ZeroProductSemiring (GF' p n f)

instance
  (KnownNat n, Reifies p Integer, Reifies f (Unipol (F p))) =>
  UnitNormalForm (GF' p n f)

instance
  (KnownNat n, Reifies p Integer, Reifies f (Unipol (F p))) =>
  IntegralDomain (GF' p n f)

instance
  (KnownNat n, Reifies p Integer, Reifies f (Unipol (F p))) =>
  GCDDomain (GF' p n f)

instance
  (KnownNat n, Reifies p Integer, Reifies f (Unipol (F p))) =>
  UFD (GF' p n f)

instance
  (KnownNat n, Reifies p Integer, Reifies f (Unipol (F p))) =>
  PID (GF' p n f)

instance
  (KnownNat n, Reifies p Integer, Reifies f (Unipol (F p))) =>
  Euclidean (GF' p n f)

instance (Reifies p Integer, Reifies f (Unipol (F p)), KnownNat n) => P.Num (GF' p n f) where
  + :: GF' p n f -> GF' p n f -> GF' p n f
(+) = GF' p n f -> GF' p n f -> GF' p n f
forall r. Additive r => r -> r -> r
(NA.+)
  (-) = GF' p n f -> GF' p n f -> GF' p n f
forall r. Group r => r -> r -> r
(NA.-)
  negate :: GF' p n f -> GF' p n f
negate = GF' p n f -> GF' p n f
forall r. Group r => r -> r
NA.negate
  * :: GF' p n f -> GF' p n f -> GF' p n f
(*) = GF' p n f -> GF' p n f -> GF' p n f
forall r. Multiplicative r => r -> r -> r
(NA.*)
  fromInteger :: Integer -> GF' p n f
fromInteger = Integer -> GF' p n f
forall r. Ring r => Integer -> r
NA.fromInteger
  abs :: GF' p n f -> GF' p n f
abs = String -> GF' p n f -> GF' p n f
forall a. HasCallStack => String -> a
error String
"not defined"
  signum :: GF' p n f -> GF' p n f
signum = String -> GF' p n f -> GF' p n f
forall a. HasCallStack => String -> a
error String
"not defined"

instance (Reifies p Integer, Reifies f (Unipol (F p)), KnownNat n) => P.Fractional (GF' p n f) where
  fromRational :: Rational -> GF' p n f
fromRational Rational
u = Integer -> GF' p n f
forall r. Num r => Integer -> r
fromInteger (Rational -> Integer
forall a. Ratio a -> a
Rat.numerator Rational
u) GF' p n f -> GF' p n f -> GF' p n f
forall r. Division r => r -> r -> r
/ Integer -> GF' p n f
forall r. Num r => Integer -> r
fromInteger (Rational -> Integer
forall a. Ratio a -> a
Rat.denominator Rational
u)
  / :: GF' p n f -> GF' p n f -> GF' p n f
(/) = GF' p n f -> GF' p n f -> GF' p n f
forall r. Division r => r -> r -> r
(/)
  recip :: GF' p n f -> GF' p n f
recip = GF' p n f -> GF' p n f
forall r. Division r => r -> r
recip

-- | @generateIrreducible p n@ generates irreducible polynomial over F_@p@ of degree @n@.
generateIrreducible ::
  (MonadRandom m, Random k, FiniteField k, Eq k) =>
  proxy k ->
  Natural ->
  m (Unipol k)
generateIrreducible :: proxy k -> Natural -> m (Unipol k)
generateIrreducible proxy k
p Natural
n =
  (Unipol k -> Bool) -> m (Unipol k) -> m (Unipol k)
forall (m :: * -> *) a. Monad m => (a -> Bool) -> m a -> m a
iterateUntil (\Unipol k
f -> (Natural -> Bool) -> [Natural] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Natural
i -> Unipol k
forall r. Unital r => r
one Unipol k -> Unipol k -> Bool
forall a. Eq a => a -> a -> Bool
== Unipol k -> Unipol k -> Unipol k
forall d. GCDDomain d => d -> d -> d
gcd (Unipol k
forall r. CoeffRing r => Unipol r
varX Unipol k -> Natural -> Unipol k
forall r. Unital r => r -> Natural -> r
^ (proxy k -> Natural
forall k (proxy :: * -> *). FiniteField k => proxy k -> Natural
order proxy k
p Natural -> Natural -> Natural
forall r. Unital r => r -> Natural -> r
^ Natural
i) Unipol k -> Unipol k -> Unipol k
forall r. Group r => r -> r -> r
- Unipol k
forall r. CoeffRing r => Unipol r
varX) Unipol k
f) [Natural
1 .. Natural
n Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
2]) (m (Unipol k) -> m (Unipol k)) -> m (Unipol k) -> m (Unipol k)
forall a b. (a -> b) -> a -> b
$ do
    [k]
cs <- Int -> m k -> m [k]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) m k
forall (m :: * -> *) a. (MonadRandom m, Random a) => m a
getRandom
    let f :: Unipol k
f = Unipol k
forall r. CoeffRing r => Unipol r
varX Unipol k -> Natural -> Unipol k
forall r. Unital r => r -> Natural -> r
^ Natural
n Unipol k -> Unipol k -> Unipol k
forall r. Additive r => r -> r -> r
+ [Unipol k] -> Unipol k
forall (f :: * -> *) m. (Foldable f, Monoidal m) => f m -> m
sum [Coefficient (Unipol k) -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff k
Coefficient (Unipol k)
c Unipol k -> Unipol k -> Unipol k
forall r. Multiplicative r => r -> r -> r
* (Unipol k
forall r. CoeffRing r => Unipol r
varX Unipol k -> Natural -> Unipol k
forall r. Unital r => r -> Natural -> r
^ Natural
i) | k
c <- [k]
cs | Natural
i <- [Natural
0 .. Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
P.- Natural
1]]
    Unipol k -> m (Unipol k)
forall (m :: * -> *) a. Monad m => a -> m a
return Unipol k
f

withIrreducible ::
  forall p a.
  KnownNat p =>
  Unipol (F p) ->
  (forall f (n :: Nat). (Reifies f (Unipol (F p))) => Proxy (GF' p n f) -> a) ->
  a
withIrreducible :: Unipol (F p)
-> (forall f (n :: Nat).
    Reifies f (Unipol (F p)) =>
    Proxy (GF' p n f) -> a)
-> a
withIrreducible Unipol (F p)
r forall f (n :: Nat).
Reifies f (Unipol (F p)) =>
Proxy (GF' p n f) -> a
f =
  case Natural -> SomeSNat
toSomeSNat (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> Int -> Natural
forall a b. (a -> b) -> a -> b
$ Unipol (F p) -> Int
forall poly. IsPolynomial poly => poly -> Int
totalDegree' Unipol (F p)
r) of
    SomeSNat SNat n
sn ->
      SNat n -> (KnownNat n => a) -> a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn ((KnownNat n => a) -> a) -> (KnownNat n => a) -> a
forall a b. (a -> b) -> a -> b
$
        Unipol (F p)
-> (forall s. Reifies s (Unipol (F p)) => Proxy s -> a) -> a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Unipol (F p)
r (Proxy (GF' p n s) -> a
forall f (n :: Nat).
Reifies f (Unipol (F p)) =>
Proxy (GF' p n f) -> a
f (Proxy (GF' p n s) -> a)
-> (Proxy s -> Proxy (GF' p n s)) -> Proxy s -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (F p) -> SNat n -> Proxy s -> Proxy (GF' p n s)
forall k (p :: k) (n :: Nat) f.
Proxy (F p) -> SNat n -> Proxy f -> Proxy (GF' p n f)
proxyGF' (forall k (t :: k). Proxy t
forall k (n :: k). Proxy (F n)
Proxy :: Proxy (F n)) SNat n
sn)

reifyGF' ::
  MonadRandom m =>
  Natural ->
  Natural ->
  ( forall (p :: TL.Nat) (f :: Type) (n :: TL.Nat).
    (Reifies p Integer, Reifies f (Unipol (F p))) =>
    Proxy (GF' p n f) ->
    a
  ) ->
  m a
reifyGF' :: Natural
-> Natural
-> (forall (p :: Nat) f (n :: Nat).
    (Reifies p Integer, Reifies f (Unipol (F p))) =>
    Proxy (GF' p n f) -> a)
-> m a
reifyGF' Natural
p Natural
n forall (p :: Nat) f (n :: Nat).
(Reifies p Integer, Reifies f (Unipol (F p))) =>
Proxy (GF' p n f) -> a
f = Integer
-> (forall (p :: Nat). KnownNat p => Proxy (F p) -> m a) -> m a
forall a.
Integer -> (forall (p :: Nat). KnownNat p => Proxy (F p) -> a) -> a
reifyPrimeField (Natural -> Integer
forall a. Integral a => a -> Integer
P.toInteger Natural
p) ((forall (p :: Nat). KnownNat p => Proxy (F p) -> m a) -> m a)
-> (forall (p :: Nat). KnownNat p => Proxy (F p) -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \Proxy (F p)
pxy -> do
  Unipol (F p)
mpol <- Proxy (F p) -> Natural -> m (Unipol (F p))
forall (m :: * -> *) k (proxy :: * -> *).
(MonadRandom m, Random k, FiniteField k, Eq k) =>
proxy k -> Natural -> m (Unipol k)
generateIrreducible Proxy (F p)
pxy Natural
n
  case Natural -> SomeSNat
toSomeSNat (Natural -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
p) of
    SomeSNat SNat n
sp -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ SNat n -> (KnownNat n => a) -> a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sp ((KnownNat n => a) -> a) -> (KnownNat n => a) -> a
forall a b. (a -> b) -> a -> b
$ Unipol (F p)
-> (forall f (n :: Nat).
    Reifies f (Unipol (F p)) =>
    Proxy (GF' p n f) -> a)
-> a
forall (p :: Nat) a.
KnownNat p =>
Unipol (F p)
-> (forall f (n :: Nat).
    Reifies f (Unipol (F p)) =>
    Proxy (GF' p n f) -> a)
-> a
withIrreducible Unipol (F p)
mpol forall f (n :: Nat).
Reifies f (Unipol (F p)) =>
Proxy (GF' p n f) -> a
forall (p :: Nat) f (n :: Nat).
(Reifies p Integer, Reifies f (Unipol (F p))) =>
Proxy (GF' p n f) -> a
f

linearRepGF :: GF' p n f -> V.Vector (F p)
linearRepGF :: GF' p n f -> Vector (F p)
linearRepGF = Sized Vector n (F p) -> Vector (F p)
forall (f :: * -> *) (n :: Nat) a. Sized f n a -> f a
SV.unsized (Sized Vector n (F p) -> Vector (F p))
-> (GF' p n f -> Sized Vector n (F p)) -> GF' p n f -> Vector (F p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GF' p n f -> Sized Vector n (F p)
forall k (p :: k) (n :: Nat) f. GF' p n f -> Sized n (F p)
runGF'

linearRepGF' :: GF' p n f -> V.Vector Integer
linearRepGF' :: GF' p n f -> Vector Integer
linearRepGF' = (F p -> Integer) -> Vector (F p) -> Vector Integer
forall a b. (a -> b) -> Vector a -> Vector b
V.map F p -> Integer
forall k (p :: k). F p -> Integer
naturalRepr (Vector (F p) -> Vector Integer)
-> (GF' p n f -> Vector (F p)) -> GF' p n f -> Vector Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GF' p n f -> Vector (F p)
forall k (p :: k) (n :: Nat) f. GF' p n f -> Vector (F p)
linearRepGF

withGF' ::
  MonadRandom m =>
  Natural ->
  Natural ->
  ( forall (p :: TL.Nat) f (n :: TL.Nat).
    (Reifies p Integer, Reifies f (Unipol (F p))) =>
    GF' p n f
  ) ->
  m (V.Vector Integer)
withGF' :: Natural
-> Natural
-> (forall (p :: Nat) f (n :: Nat).
    (Reifies p Integer, Reifies f (Unipol (F p))) =>
    GF' p n f)
-> m (Vector Integer)
withGF' Natural
p Natural
n forall (p :: Nat) f (n :: Nat).
(Reifies p Integer, Reifies f (Unipol (F p))) =>
GF' p n f
f = Natural
-> Natural
-> (forall (p :: Nat) f (n :: Nat).
    (Reifies p Integer, Reifies f (Unipol (F p))) =>
    Proxy (GF' p n f) -> Vector Integer)
-> m (Vector Integer)
forall (m :: * -> *) a.
MonadRandom m =>
Natural
-> Natural
-> (forall (p :: Nat) f (n :: Nat).
    (Reifies p Integer, Reifies f (Unipol (F p))) =>
    Proxy (GF' p n f) -> a)
-> m a
reifyGF' Natural
p Natural
n ((forall (p :: Nat) f (n :: Nat).
  (Reifies p Integer, Reifies f (Unipol (F p))) =>
  Proxy (GF' p n f) -> Vector Integer)
 -> m (Vector Integer))
-> (forall (p :: Nat) f (n :: Nat).
    (Reifies p Integer, Reifies f (Unipol (F p))) =>
    Proxy (GF' p n f) -> Vector Integer)
-> m (Vector Integer)
forall a b. (a -> b) -> a -> b
$ (F p -> Integer) -> Vector (F p) -> Vector Integer
forall a b. (a -> b) -> Vector a -> Vector b
V.map F p -> Integer
forall k (p :: k). F p -> Integer
naturalRepr (Vector (F p) -> Vector Integer)
-> (Proxy (GF' p n f) -> Vector (F p))
-> Proxy (GF' p n f)
-> Vector Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GF' p n f -> Vector (F p)
forall k (p :: k) (n :: Nat) f. GF' p n f -> Vector (F p)
linearRepGF (GF' p n f -> Vector (F p))
-> (Proxy (GF' p n f) -> GF' p n f)
-> Proxy (GF' p n f)
-> Vector (F p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GF' p n f -> Proxy (GF' p n f) -> GF' p n f
forall a (proxy :: * -> *). a -> proxy a -> a
asProxyTypeOf GF' p n f
forall (p :: Nat) f (n :: Nat).
(Reifies p Integer, Reifies f (Unipol (F p))) =>
GF' p n f
f

proxyGF' :: Proxy (F p) -> SNat n -> Proxy f -> Proxy (GF' p n f)
proxyGF' :: Proxy (F p) -> SNat n -> Proxy f -> Proxy (GF' p n f)
proxyGF' Proxy (F p)
_ SNat n
_ Proxy f
Proxy = Proxy (GF' p n f)
forall k (t :: k). Proxy t
Proxy

-- | Type-constraint synonym to work with Galois field.
class (KnownNat n, KnownNat p, Reifies f (Unipol (F p))) => IsGF' p n f

instance (KnownNat n, KnownNat p, Reifies f (Unipol (F p))) => IsGF' p n f

instance (KnownNat n, IsGF' p n f) => ZeroProductSemiring (GF' p n f)

instance (KnownNat n, IsGF' p n f) => FiniteField (GF' p n f) where
  power :: proxy (GF' p n f) -> Natural
power proxy (GF' p n f)
_ = Natural -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Natural) -> Natural -> Natural
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n)
  elements :: proxy (GF' p n f) -> [GF' p n f]
elements proxy (GF' p n f)
_ =
    let sn :: SNat n
sn = SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n
     in (Sized n (F p) -> GF' p n f) -> [Sized n (F p)] -> [GF' p n f]
forall a b. (a -> b) -> [a] -> [b]
P.map Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' ([Sized n (F p)] -> [GF' p n f]) -> [Sized n (F p)] -> [GF' p n f]
forall a b. (a -> b) -> a -> b
$
          Sized Vector n [F p] -> [Sized n (F p)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
T.sequence (Sized Vector n [F p] -> [Sized n (F p)])
-> Sized Vector n [F p] -> [Sized n (F p)]
forall a b. (a -> b) -> a -> b
$
            SNat n -> [F p] -> Sized Vector n [F p]
forall (f :: * -> *) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
SV.replicate SNat n
sn ([F p] -> Sized Vector n [F p]) -> [F p] -> Sized Vector n [F p]
forall a b. (a -> b) -> a -> b
$ Proxy (F p) -> [F p]
forall k (proxy :: * -> *). FiniteField k => proxy k -> [k]
elements Proxy (F p)
forall k (t :: k). Proxy t
Proxy

primitive' :: forall p n f. (IsGF' p n f, 1 <= n) => GF' p n f
primitive' :: GF' p n f
primitive' = SNat (1 + n) -> (KnownNat (1 + n) => GF' p n f) -> GF' p n f
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (KnownNat 1 => SNat 1
forall (n :: Nat). KnownNat n => SNat n
sNat @1 SNat 1 -> SNat n -> SNat (1 + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n)) ((KnownNat (1 + n) => GF' p n f) -> GF' p n f)
-> (KnownNat (1 + n) => GF' p n f) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f) -> Sized n (F p) -> GF' p n f
forall a b. (a -> b) -> a -> b
$ Unipol (F p) -> Sized n (F p)
forall (n :: Nat) r.
(CoeffRing r, KnownNat n) =>
Unipol r -> Sized n r
polyToVec (Unipol (F p) -> Sized n (F p)) -> Unipol (F p) -> Sized n (F p)
forall a b. (a -> b) -> a -> b
$ Ordinal (Arity (Unipol (F p))) -> Unipol (F p)
forall poly. IsPolynomial poly => Ordinal (Arity poly) -> poly
var [od|0|]

primitive :: forall p n. (IsGF' p n (Conway p n), 1 <= n) => GF p n
primitive :: GF p n
primitive = GF p n
forall (p :: Nat) (n :: Nat) f. (IsGF' p n f, 1 <= n) => GF' p n f
primitive'

-- | Conway polynomial (if definition is known).
conway ::
  forall p n.
  ConwayPolynomial p n =>
  SNat p ->
  SNat n ->
  Unipol (F p)
conway :: SNat p -> SNat n -> Unipol (F p)
conway = SNat p -> SNat n -> Unipol (F p)
forall (p :: Nat) (n :: Nat) (proxy :: Nat -> *).
ConwayPolynomial p n =>
proxy p -> proxy n -> Unipol (F p)
conwayPolynomial

instance IsGF' p n f => Random (GF' p n f) where
  random :: g -> (GF' p n f, g)
random =
    Rand g (GF' p n f) -> g -> (GF' p n f, g)
forall g a. Rand g a -> g -> (a, g)
runRand (Rand g (GF' p n f) -> g -> (GF' p n f, g))
-> Rand g (GF' p n f) -> g -> (GF' p n f, g)
forall a b. (a -> b) -> a -> b
$
      Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f)
-> RandT g Identity (Sized n (F p)) -> Rand g (GF' p n f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sized Vector n (RandT g Identity (F p))
-> RandT g Identity (Sized n (F p))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (RandT g Identity (F p) -> Sized Vector n (RandT g Identity (F p))
forall (f :: * -> *) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
SV.replicate' RandT g Identity (F p)
forall (m :: * -> *) a. (MonadRandom m, Random a) => m a
getRandom)
  randomR :: (GF' p n f, GF' p n f) -> g -> (GF' p n f, g)
randomR (GF' Sized n (F p)
ls, GF' Sized n (F p)
rs) =
    Rand g (GF' p n f) -> g -> (GF' p n f, g)
forall g a. Rand g a -> g -> (a, g)
runRand (Rand g (GF' p n f) -> g -> (GF' p n f, g))
-> Rand g (GF' p n f) -> g -> (GF' p n f, g)
forall a b. (a -> b) -> a -> b
$
      Sized n (F p) -> GF' p n f
forall k (p :: k) (n :: Nat) f. Sized n (F p) -> GF' p n f
GF' (Sized n (F p) -> GF' p n f)
-> RandT g Identity (Sized n (F p)) -> Rand g (GF' p n f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sized Vector n (RandT g Identity (F p))
-> RandT g Identity (Sized n (F p))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((F p -> F p -> RandT g Identity (F p))
-> Sized n (F p)
-> Sized n (F p)
-> Sized Vector n (RandT g Identity (F p))
forall (f :: * -> *) (n :: Nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
SV.zipWithSame (((F p, F p) -> RandT g Identity (F p))
-> F p -> F p -> RandT g Identity (F p)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (F p, F p) -> RandT g Identity (F p)
forall (m :: * -> *) a. (MonadRandom m, Random a) => (a, a) -> m a
getRandomR) Sized n (F p)
ls Sized n (F p)
rs)