{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module GF
    ( Z
    , S
    , Nat
    , Prime
    , GF
    , GF2
    , GF3
    , GF5
    --, gf
    ) where

import Data.Ratio (denominator, numerator)
--import Language.Haskell.TH

-----------------------------------------------------------------------------

data Z
data S n

newtype NatInt n = NatInt Int

class Nat n where
    natInt :: NatInt n

instance Nat Z where
    natInt = NatInt 0

instance Nat n => Nat (S n) where
    natInt = case (natInt :: NatInt n) of
             NatInt n -> NatInt (n+1)

-----------------------------------------------------------------------------

class Nat n => Prime n
instance (Nat n, PrimeTest (S (S n)) (S (S n))) => Prime (S (S n))

-- p は {x | 1<x<a} では割り切れない
-- 実装は手抜き
class PrimeTest p a
instance PrimeTest p (S (S Z))
instance (PrimeTest p (S (S a)), NotDivide (S (S a)) p)
    => PrimeTest p (S (S (S a)))

-- aはbを割り切らない
class NotDivide a b
instance NotDivide' a a b => NotDivide a b
class NotDivide' a x y
instance NotDivide' (S a) (S y) Z 
instance NotDivide' (S a) a y => NotDivide' (S a) Z (S y)
instance NotDivide' (S a) x y => NotDivide' (S a) (S x) (S y)

-----------------------------------------------------------------------------

newtype GF p = GF Int deriving Eq

fromInt :: forall p. Nat p => Int -> GF p
fromInt a =
    case (natInt :: NatInt p) of
    NatInt p -> GF (a `mod` p)

toInt :: GF p -> Int
toInt (GF x) = x

instance Nat p => Show (GF p) where
    showsPrec n (GF x) = showsPrec n x

instance Nat p => Read (GF p) where
    readsPrec n s = [(fromInt a, s') | (a,s') <- readsPrec n s]

instance Nat p => Num (GF p) where
    GF a + GF b   = fromInt $ a+b
    GF a * GF b   = fromInt $ a*b
    GF a - GF b   = fromInt $ a-b
    negate (GF a) = fromInt $ negate a
    abs a         = a
    signum _      = 1
    fromInteger   = fromInt . fromIntegral

instance Nat p => Ord (GF p) where
    GF a `compare` GF b = a `compare` b
    GF a `max` GF b = GF (a `max` b)
    GF a `min` GF b = GF (a `min` b)

instance Nat p => Bounded (GF p) where
    minBound = 0
    maxBound =
        case (natInt :: NatInt p) of
        NatInt p -> GF (p - 1)

instance Nat p => Real (GF p) where
    toRational (GF x) = toRational x

instance Prime p => Fractional (GF p) where
    fromRational r =
        fromInteger (numerator r) / fromInteger (denominator r)
    _ / 0 = error "divide by zero"
    (GF x) / (GF y) =
        case (natInt :: NatInt p) of
        NatInt p ->
            case exGCD y p of
            (a,_,_) -> fromInt (a*x)

-- 拡張ユークリッド互除法
exGCD :: Int -> Int -> (Int,Int,Int)
exGCD x y = loop x y 1 0 0 1
    where loop x y a0 a1 b0 b1
              | y == 0 = (a0,b0,x)
              | otherwise = loop y r a1 (a0 - q*a1) b1 (b0 - q*b1)
                  where (q,r) = x `divMod` y

instance Nat p => Enum (GF p) where
    toEnum x
        | toInt (minBound :: GF p) <= x
          && x <= toInt (maxBound :: GF p) = fromInt x
        | otherwise = error "GF.toEnum: bad argument"
    fromEnum (GF x) = x

-----------------------------------------------------------------------------

type GF2 = GF (S (S Z))
type GF3 = GF (S (S (S Z)))
type GF5 = GF (S (S (S (S (S Z)))))

-----------------------------------------------------------------------------

{-
gf :: Int -> Type
gf x = AppT (ConT (mkName "GF.GF")) (f x)
    where f 0     = ConT (mkName "GF.Z")
          f (x+1) = AppT (ConT (mkName "GF.S")) (f x)
-}

-----------------------------------------------------------------------------