{-# LANGUAGE RebindableSyntax,QuasiQuotes #-}

-- | This module contains most of the math types not directly related to linear algebra
--
-- FIXME: there is probably a better name for this
module SubHask.Algebra.Group
    where

import Control.Monad
import qualified Prelude as P

import SubHask.Algebra
import SubHask.Category
import SubHask.Mutable
import SubHask.SubType
import SubHask.Internal.Prelude
import SubHask.TemplateHaskell.Deriving

-------------------------------------------------------------------------------
-- non-negative objects

newtype NonNegative t = NonNegative { unNonNegative :: t }

deriveHierarchy ''NonNegative [ ''Enum, ''Boolean, ''Rig, ''Metric ]

instance (Ord t, Group t) => Cancellative (NonNegative t) where
    (NonNegative t1)-(NonNegative t2) = if diff>zero
        then NonNegative diff
        else NonNegative zero
        where
            diff=t1-t2

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

{-
newtype a +> b = HomHask { unHomHask :: a -> b }
infixr +>

unsafeHomHask2 :: (a -> b -> c) -> (a +> b +> c)
unsafeHomHask2 f = HomHask (\a -> HomHask $ \b -> f a b)

instance Category (+>) where
    type ValidCategory (+>) a = ()
    id = HomHask id
    (HomHask a).(HomHask b) = HomHask $ a.b

instance Sup (+>) (->) (->)
instance Sup (->) (+>) (->)
instance (+>) <: (->) where
    embedType_ = Embed2 unHomHask

instance Monoidal (+>) where
    type Tensor (+>) = (,)
    tensor = unsafeHomHask2 $ \a b -> (a,b)

instance Braided (+>) where
    braid  = HomHask $ \(a,b) -> (b,a)
    unbraid = braid

instance Closed (+>) where
    curry (HomHask f) = HomHask $ \ a -> HomHask $ \b -> f (a,b)
    uncurry (HomHask f) = HomHask $ \ (a,b) -> unHomHask (f a) b

mkSubtype [t|Int|] [t|Integer|] 'toInteger

[subhask|
poop :: (Semigroup' g, Ring g) => g +> g
poop = (+:1)
|]

class Semigroup' a where
    (+:) :: a +> a +> a

instance Semigroup' Int where (+:) = unsafeHomHask2 (+)

instance Semigroup' [a] where (+:) = unsafeHomHask2 (+)

f :: Integer +> Integer
f = HomHask $ \i -> i+1

n1 = NonNegative 5 :: NonNegative Int
n2 = NonNegative 3 :: NonNegative Int
i1 = 5 :: Int
i2 = 3 :: Int
j1 = 5 :: Integer
j2 = 3 :: Integer
-}

-------------------------------------------------------------------------------
-- integers modulo n

-- | Maps members of an equivalence class into the "canonical" element.
class Quotient a (b::k) where
    mkQuotient :: a -> a/b

-- | The type of equivalence classes created by a mod b.
newtype (/) (a :: *) (b :: k) = Mod a

-- mkDefaultMutable [t| forall a b. a/b |]

-- newtype instance Mutable m (a/b) = Mutable_Mod (Mutable m a)

instance (Quotient a b, Arbitrary a) => Arbitrary (a/b) where
    arbitrary = liftM mkQuotient arbitrary

deriveHierarchyFiltered ''(/) [ ''Eq_, ''P.Ord ] [''Arbitrary]

instance (Semigroup a, Quotient a b) => Semigroup (a/b) where
    (Mod z1) + (Mod z2) = mkQuotient $ z1 + z2

instance (Abelian a, Quotient a b) => Abelian (a/b)

instance (Monoid a, Quotient a b) => Monoid (a/b)
    where zero = Mod zero

instance (Cancellative a, Quotient a b) => Cancellative (a/b) where
    (Mod i1)-(Mod i2) = mkQuotient $ i1-i2

instance (Group a, Quotient a b) => Group (a/b) where
    negate (Mod i) = mkQuotient $ negate i

instance (Rg a, Quotient a b) => Rg (a/b) where
    (Mod z1)*(Mod z2) = mkQuotient $ z1 * z2

instance (Rig a, Quotient a b) => Rig (a/b) where
    one = Mod one

instance (Ring a, Quotient a b) => Ring (a/b) where
    fromInteger i = mkQuotient $ fromInteger i

type instance ((a/b)><c) = (a><c)/b

instance (Module a, Quotient a b) => Module (a/b) where
    (Mod a) .*  r       = mkQuotient $ a .*  r

-- | The type of integers modulo n
type Z (n::Nat) = Integer/n

instance KnownNat n => Quotient Int n
    where
        mkQuotient i = Mod $ i `P.mod` (fromIntegral $ natVal (Proxy::Proxy n))

instance KnownNat n => Quotient Integer n
    where
        mkQuotient i = Mod $ i `P.mod` (natVal (Proxy::Proxy n))

-- | Extended Euclid's algorithm is used to calculate inverses in modular arithmetic
extendedEuclid :: (Eq t, Integral t) => t -> t -> (t,t,t,t,t,t)
extendedEuclid a b = go zero one one zero b a
    where
        go s1 s0 t1 t0 r1 r0 = if r1==zero
            then (s1,s0,t1,t0,undefined,r0)
            else go s1' s0' t1' t0' r1' r0'
            where
                q = r0 `div` r1
                (r0', r1') = (r1,r0-q*r1)
                (s0', s1') = (s1,s0-q*s1)
                (t0', t1') = (t1,t0-q*t1)

-------------------------------------------------------------------------------
-- example: Galois field

-- | @Galois p k@ is the type of integers modulo p^k, where p is prime.
-- All finite fields have this form.
--
-- See wikipedia <https://en.wikipedia.org/wiki/Finite_field> for more details.
--
-- FIXME: Many arithmetic operations over Galois Fields can be implemented more efficiently than the standard operations.
-- See <http://en.wikipedia.org/wiki/Finite_field_arithmetic>.
newtype Galois (p::Nat) (k::Nat) = Galois (Z (p^k))

type instance Galois p k >< Integer = Galois p k

deriveHierarchy ''Galois [''Eq_,''Ring]

instance KnownNat (p^k) => Module  (Galois p k) where
    z  .*   i = Galois (Mod i) * z

instance (Prime p, KnownNat (p^k)) => Field (Galois p k) where
    reciprocal (Galois (Mod i)) = Galois $ mkQuotient $ t
        where
            (_,_,_,t,_,_) = extendedEuclid n i
            n = natVal (Proxy::Proxy (p^k))

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

class Prime (n::Nat)
instance Prime 1
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

-------------------------------------------------------------------------------
-- the symmetric group

-- | The symmetric group is one of the simplest and best studied finite groups.
-- It is efficiently implemented as a "BijectiveT SparseFunction (Z n) (Z n)".
-- See <https://en.wikipedia.org/wiki/Symmetric_group>

-- newtype Sym (n::Nat) = Sym (BijectiveT SparseFunction (Z n) (Z n))
--
-- instance KnownNat n => Monoid (Sym n) where
--     zero = Sym id
--     (Sym s1)+(Sym s2) = Sym $ s1.s2
--
-- instance KnownNat n => Group (Sym n) where
--     negate (Sym s) = Sym $ inverse s

-------------------------------------------------------------------------------
-- | The GrothendieckGroup is a general way to construct groups from cancellative semigroups.
--
-- FIXME: How should this be related to the Ratio type?
--
-- See <http://en.wikipedia.org/wiki/Grothendieck_group wikipedia> for more details.
data GrothendieckGroup g where
    GrotheindieckGroup :: Cancellative g => g -> GrothendieckGroup g

-------------------------------------------------------------------------------
-- the vedic square

-- | The Vedic Square always forms a monoid,
-- and sometimes forms a group depending on the value of "n".
-- (The type system isn't powerful enough to encode these special cases.)
--
-- See <https://en.wikipedia.org/wiki/Vedic_square wikipedia> for more detail.
newtype VedicSquare (n::Nat) = VedicSquare (Z n)

deriveHierarchy ''VedicSquare [''Eq_]

instance KnownNat n => Semigroup (VedicSquare n) where
    (VedicSquare v1)+(VedicSquare v2) = VedicSquare $ v1*v2

instance KnownNat n => Monoid (VedicSquare n) where
    zero = VedicSquare one

------------------------------------------------------------------------------
-- Minkowski addition

-- | TODO: implement
-- More details available at <https://en.wikipedia.org/wiki/Minkowski_addition wikipedia>.