{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeData #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.YAP.Quotient
-- Copyright   :  (c) Ross Paterson 2021
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  R.Paterson@city.ac.uk
-- Stability   :  provisional
-- Portability :  GHC type extensions
--
-- Quotient of a Euclidean ring by the principal ideal generated by a
-- specified value.
--
-- Special cases include modular arithmetic (cyclic groups), algebraic
-- extensions and finite fields.
--
-----------------------------------------------------------------------------

module Data.YAP.Quotient (
    -- * Statically determined values
    StaticValue(..), StaticType, Known(..),
    Irreducible, Prime,
    -- * Quotient by a static value
    Quotient, coset, representative, powers,
    -- * Examples
    SimpleExtension,
    Qi,
    Z,
    PrimePower, ConwayEncoded,
    FiniteField(..),
    ) where

import Prelude.YAP
import Data.YAP.Algebra
import Data.YAP.Polynomial

import Data.Kind (Type)
import Data.List (unfoldr)
import Data.Proxy
import GHC.TypeLits

-- | A static value
type data StaticValue
    = N Nat
        -- ^ A natural number as a static value
    | SqrtMinusOne Type
        -- ^ The polynomial \(x^2 + 1\), whose root is \(i = \sqrt{-1}\).
    | ConwayPolynomial Nat Nat
        -- ^ Conway polynomials define for each prime \(p\)
        -- and each \(k > 1\) a standard primitive polynomial
        -- over \(GF(p)\) of degree \(k\).  These are used
        -- to provide a canonical definition of \(GF(p^k)\).  See
        -- <https://www.math.rwth-aachen.de/~Frank.Luebeck/data/ConwayPol/index.html>
        -- for a long list.

-- | The type of the statically determined element
type family StaticType (v :: StaticValue) :: Type

-- | @v@ denotes a statically determined element of type @StaticType v@.
class Known v where
    value :: Proxy v -> StaticType v

type instance StaticType (N n) = Integer

instance (KnownNat n) => Known (N n) where
    value = natVal . getNProxy

getNProxy :: Proxy (N n) -> Proxy n
getNProxy _ = Proxy

-- | The value is an irreducible element: it is not zero or a unit,
-- and is not a product of two non-units.
class (Known v) => Irreducible v

-- | prime numbers
class (KnownNat p) => Prime p

-- primes less than 100
instance Prime 2
instance Prime 3
instance Prime 5
instance Prime 7
instance Prime 11
instance Prime 13
instance Prime 17
instance Prime 19
instance Prime 23
instance Prime 29
instance Prime 31
instance Prime 37
instance Prime 41
instance Prime 43
instance Prime 47
instance Prime 53
instance Prime 59
instance Prime 61
instance Prime 67
instance Prime 71
instance Prime 73
instance Prime 79
instance Prime 83
instance Prime 89
instance Prime 97

instance (Prime p) => Irreducible (N p)

-- | Quotient of @a@ by the principal ideal \(\langle v \rangle\)
-- generated by the static value \(v\) (consisting of the multiples
-- of \(v\)).  The elements of the quotient are the additive cosets of
-- \(\langle v \rangle\) with the induced operations.
newtype Quotient a (v::StaticValue) = Coset a
    deriving (Eq)

instance (Show a) => Show (Quotient a v) where
    showsPrec p (Coset x) = showParen (p > app_prec) $
        showString "coset " . showsPrec (app_prec+1) x
      where app_prec = 10

-- | Addition modulo @v@
instance (Known v, a ~ StaticType v, Euclidean a) =>
        AdditiveMonoid (Quotient a v) where
    Coset x + Coset y = coset (x + y)
    zero = Coset zero

-- | Subtraction modulo @v@
instance (Known v, a ~ StaticType v, Euclidean a, AbelianGroup a) =>
        AbelianGroup (Quotient a v) where
    Coset x - Coset y = coset (x - y)

-- | Multiplication modulo @v@
instance (Known v, a ~ StaticType v, Euclidean a) =>
        Semiring (Quotient a v) where
    Coset x * Coset y = coset (x * y)
    one = coset one
    fromNatural i = coset (fromNatural i)

instance (Known v, a ~ StaticType v, Euclidean a, Ring a) =>
        Ring (Quotient a v) where
    fromInteger i = coset (fromInteger i)

instance (Irreducible v, a ~ StaticType v,
        Eq a, StandardAssociate a, Euclidean a, Ring a) =>
        DivisionSemiring (Quotient a v) where
    recip = recipProxy Proxy

instance (Irreducible v, a ~ StaticType v,
        Eq a, StandardAssociate a, Euclidean a, Ring a) =>
        Semifield (Quotient a v)

instance (Irreducible v, a ~ StaticType v,
        Eq a, StandardAssociate a, Euclidean a, Ring a) =>
        DivisionRing (Quotient a v)

instance (Irreducible v, a ~ StaticType v,
        Eq a, StandardAssociate a, Euclidean a, Ring a) =>
        Field (Quotient a v)

recipProxy ::
    (Irreducible v, a ~ StaticType v,
     Eq a, AbelianGroup a, StandardAssociate a, Euclidean a) =>
        Proxy v -> Quotient a v -> Quotient a v
recipProxy p (Coset x)
  | x == zero = error "reciprocal of zero"
  | otherwise = cosetProxy p (fst (bezout x (value p)))

-- | (semi)ring homomorphism yielding the coset of \(\langle v \rangle\)
-- containing \(x\).
coset :: (Known v, a ~ StaticType v, Euclidean a) => a -> Quotient a v
coset = cosetProxy Proxy

cosetProxy :: (Known v, a ~ StaticType v, Euclidean a) =>
    Proxy v -> a -> Quotient a v
cosetProxy p x = Coset (x `mod` value p)

-- | The representative element of the coset, a value modulo \(v\).
--
-- prop> representative (coset x) = x `mod` v
--
representative :: (Known v, a ~ StaticType v, Euclidean a) => Quotient a v -> a
representative (Coset x) = x

-- general examples

-- | Cyclic group of order \(n\).  This is also a ring.
-- If \(n\) is prime, it is a field, the Galois field of order \(n\),
-- or \(GF(n)\).
type Z (n::Nat) = Quotient Integer (N n)

-- | Simple algebraic extension, where @poly@ defines an irreducible
-- polynomial in @a@.  Adjoins a root of the polynomial to the field.
type SimpleExtension a poly = Quotient (Polynomial a) poly

-- | All the powers of @x@
powers :: (Eq a, Semiring a) => a -> [a]
powers x = one : takeWhile (/= one) (iterate (x*) x)

-- specific instances

type instance StaticType (SqrtMinusOne a) = Polynomial a

-- | \(x^2 + 1\)
instance (Ring a) => Known (SqrtMinusOne a) where
    value _ = fromCoefficients [1, 0, 1]

instance Irreducible (SqrtMinusOne Rational)
instance (Prime p, Mod p 4 ~ 3) => Irreducible (SqrtMinusOne (Z p))

-- | The field \({\Bbb Q}(i)\) of rationals adjoined with \(i\).
type Qi = SimpleExtension Rational (SqrtMinusOne Rational)

-- | a finite field
class (Field a) => FiniteField a where
    -- | Element that generates the multiplicative group of non-zero
    -- elements of the field
    primitiveElement :: a

instance (Prime p, KnownNat (ConwayEncoded p 1)) => FiniteField (Z p) where
    primitiveElement = primProxy Proxy Proxy

primProxy :: (Prime p, KnownNat (ConwayEncoded p 1)) =>
    Proxy p -> Proxy (ConwayEncoded p 1) -> Z p
primProxy proxy_p proxy_n = coset (p - n)
  where
    p = natVal proxy_p
    n = natVal proxy_n

instance (Prime p, KnownNat k, KnownNat (ConwayEncoded p k)) =>
        FiniteField (PrimePower p k) where
    primitiveElement = coset (fromCoefficients [0, 1])

-- | Defines a field of order \(p^k\) for prime \(p\) and \(k > 1\).
--
-- All fields of finite order have order \(p^k\) for prime \(p\), with
-- all fields of the same order isomorphic.
-- For \(k = 1\), these are \({\Bbb Z}_p\).
-- For \(k > 1\), the fields can be defined as quotients of polynomials
-- over \(GF(p)\) by any primitive polynomial of degree \(k\).
-- Conway polynomials provide a canonical representation.
type PrimePower p k = SimpleExtension (Z p) (ConwayPolynomial p k)

type instance StaticType (ConwayPolynomial p k) = Polynomial (Z p)

instance (Prime p, KnownNat k, KnownNat (ConwayEncoded p k)) =>
        Known (ConwayPolynomial p k) where
    value proxy =
        fromCoefficients (map coset (decodeProxies proxy Proxy Proxy Proxy))

instance (Prime p, KnownNat k, KnownNat (ConwayEncoded p k)) =>
    Irreducible (ConwayPolynomial p k)

-- | Decode the integer representation of a Conway polynomial
decodeProxies :: (Prime p, KnownNat k, KnownNat (ConwayEncoded p k)) =>
    Proxy (ConwayPolynomial p k) -> Proxy p -> Proxy k ->
        Proxy (ConwayEncoded p k) -> [Integer]
decodeProxies _ proxy_p proxy_k proxy_n =
    cs ++ replicate (k - length cs) 0 ++ [1]
  where
    cs = take k (unfoldr modDiv n)
    modDiv m
      | m == 0 = Nothing
      | otherwise = Just (m `mod` p, m `div` p)
    p = natVal proxy_p
    k = fromInteger (natVal proxy_k)
    n = natVal proxy_n

-- | Encoding of a Conway polynomial as an integer, obtained by removing
-- the leading term, which is always \(x^k\), and evaluating the rest
-- of the polynomial with \(x = p\).
--
-- For a prime field, i.e. \(k = 1\), the value is \(p - n\), where \(n\)
-- is the smallest primitive element of \({\Bbb Z}_p\).
type family ConwayEncoded (p::Nat) (k::Nat) :: Nat

type instance ConwayEncoded 2 1 = 1
type instance ConwayEncoded 3 1 = 1
type instance ConwayEncoded 5 1 = 3
type instance ConwayEncoded 7 1 = 4
type instance ConwayEncoded 11 1 = 9
type instance ConwayEncoded 13 1 = 11
type instance ConwayEncoded 17 1 = 14
type instance ConwayEncoded 19 1 = 17
type instance ConwayEncoded 23 1 = 18
type instance ConwayEncoded 29 1 = 27
type instance ConwayEncoded 31 1 = 28
type instance ConwayEncoded 37 1 = 35
type instance ConwayEncoded 41 1 = 35
type instance ConwayEncoded 43 1 = 40
type instance ConwayEncoded 47 1 = 42
type instance ConwayEncoded 53 1 = 51
type instance ConwayEncoded 59 1 = 57
type instance ConwayEncoded 61 1 = 59
type instance ConwayEncoded 67 1 = 65
type instance ConwayEncoded 71 1 = 64
type instance ConwayEncoded 73 1 = 68
type instance ConwayEncoded 79 1 = 76
type instance ConwayEncoded 83 1 = 81
type instance ConwayEncoded 89 1 = 86
type instance ConwayEncoded 97 1 = 92

-- | \(C_{2,2}(x) = x^2 + x + 1\)
type instance ConwayEncoded 2 2 = 3
-- | \(C_{2,3}(x) = x^3 + x + 1\)
type instance ConwayEncoded 2 3 = 3
-- | \(C_{2,4}(x) = x^4 + x + 1\)
type instance ConwayEncoded 2 4 = 3
-- | \(C_{2,5}(x) = x^5 + x^2 + 1\)
type instance ConwayEncoded 2 5 = 5
-- | \(C_{2,6}(x) = x^6 + x^4 + x^3 + x + 1\)
type instance ConwayEncoded 2 6 = 27
-- | \(C_{3,2}(x) = x^2 + 2x + 2\)
type instance ConwayEncoded 3 2 = 8
-- | \(C_{3,3}(x) = x^3 + 2x + 1\)
type instance ConwayEncoded 3 3 = 7
-- | \(C_{3,4}(x) = x^4 + 2x^3 + 2\)
type instance ConwayEncoded 3 4 = 20
-- | \(C_{5,2}(x) = x^2 + 4x + 2\)
type instance ConwayEncoded 5 2 = 22
-- | \(C_{7,2}(x) = x^2 + 6x + 3\)
type instance ConwayEncoded 7 2 = 45