{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}

-- |
-- Module      : OAlg.Structure.Additive.Definition
-- Description : definition of additive structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- additive structures, i.e. structures with a __partially__ defined addition @('+')@.
module OAlg.Structure.Additive.Definition
  (
    -- * Additive
    Additive(..), zero', Add, ForgetfulAdd

    -- * Abelian
  , Abelian(..), isZero, Abl, ForgetfulAbl
  )
  where

import qualified Prelude as A

import Control.Exception

import Data.List(repeat)
import Data.Foldable

import OAlg.Prelude

import OAlg.Data.Canonical

import OAlg.Structure.Exception
import OAlg.Structure.Oriented.Definition
import OAlg.Structure.Multiplicative.Definition
import OAlg.Structure.Fibred.Definition

--------------------------------------------------------------------------------
-- Additive -

infixl 6 +
-- | 'Fibred' structures with a __partialy__ defined __addition__ and having
-- 'zero' as the __neutral element__ of the summation. An entity of a 'Additive'
-- structure will be called a __summand__.
--
-- __Properties__ Let __@a@__ be a 'Additive' structure, then holds:
--
-- (1) #Add1#For all @r@ in __@'Root' a@__ holds: @'root' ('zero' r) '==' r@.
--
-- (2) #Add2#For all @f@ and @g@ in __@a@__ holds:
--
--     (1) #Add2_1#If @'root' f '==' 'root' g@ then @f '+' g@ is 'valid' and
--      @'root' (f '+' g) '==' 'root' f@.
--
--     (2) #Add2_2#If @'root' f '/=' 'root' g@ then @f '+' g@ is not 'valid' and its
--     evaluation will end up in a 'NotAddable'-exception.
--
-- (3) #Add3#For all @f@, @g@ in __@a@__ with @'root' f '==' 'root' g@ holds:
-- @f '+' g '==' g '+' f@.
--
-- (4) #Add4#For all @f@ in __@a@__ holds: @f '+' 'zero' ('root' f) '==' f@
--
-- (5) #Add5#For all @f@, @g@, @h@ in __@a@__ with @'root' f '==' 'root' g '==' 'root' h@
-- holds: @(f '+' g) '+' h '==' f '+' (g '+' h)@.
--
-- (6) #Add6#For all @f@ in @a@ and @n@ in __'N'__ holds:
-- @'ntimes' 0 f == 'zero' ('root' f)@ and @'ntimes' (n '+' 1) f '==' f '+' 'ntimes' n f@.
class Fibred a => Additive a where
  {-# MINIMAL zero, (+) #-}
  
  -- | the neutral element associated to each 'root'. If there is no ambiguity
  --   for @'zero' r@ we will briefly denote it by @0 r@ or just @0@.
  zero :: Root a -> a

  -- | the addition for two summands.
  (+) :: a -> a -> a

  -- | @n@ times of a summand.
  ntimes :: N -> a -> a
  ntimes N
n a
f = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Additive a => a -> a -> a
(+) (forall a. Additive a => Root a -> a
zero (forall f. Fibred f => f -> Root f
root a
f)) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. N -> [a] -> [a]
takeN N
n forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. a -> [a]
repeat forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ a
f

--------------------------------------------------------------------------------
-- Additive - Instance -

instance Additive () where
  zero :: Root () -> ()
zero Root ()
_ = ()
  ()
_ + :: () -> () -> ()
+ ()
_ = ()
  ntimes :: N -> () -> ()
ntimes N
_ ()
_ = ()

instance Additive Int where
  zero :: Root Int -> Int
zero Root Int
_ = Int
0
  + :: Int -> Int -> Int
(+) = forall a. Num a => a -> a -> a
(A.+)
  -- ntimes n i = error "nyi"

instance Additive Integer where
  zero :: Root Integer -> Integer
zero Root Integer
_ = Integer
0
  + :: Integer -> Integer -> Integer
(+) = forall a. Num a => a -> a -> a
(A.+)
  ntimes :: N -> Integer -> Integer
ntimes N
n Integer
z = forall a b. Embeddable a b => a -> b
inj N
n forall c. Multiplicative c => c -> c -> c
* Integer
z

instance Additive N where
  zero :: Root N -> N
zero Root N
_ = N
0
  + :: N -> N -> N
(+) = forall a. Num a => a -> a -> a
(A.+)
  ntimes :: N -> N -> N
ntimes = forall c. Multiplicative c => c -> c -> c
(*)

instance Additive Z where
  zero :: Root Z -> Z
zero Root Z
_ = Z
0
  + :: Z -> Z -> Z
(+) = forall a. Num a => a -> a -> a
(A.+)
  ntimes :: N -> Z -> Z
ntimes N
n Z
z = forall a b. Embeddable a b => a -> b
inj N
n forall c. Multiplicative c => c -> c -> c
* Z
z

instance Additive Q where
  zero :: Root Q -> Q
zero Root Q
_ = Q
0
  + :: Q -> Q -> Q
(+) = forall a. Num a => a -> a -> a
(A.+)
  ntimes :: N -> Q -> Q
ntimes N
n Q
q = forall a b. Embeddable a b => a -> b
inj N
n forall c. Multiplicative c => c -> c -> c
* Q
q

instance Entity p => Additive (Orientation p) where
  zero :: Root (Orientation p) -> Orientation p
zero = forall x. x -> x
id
  Orientation p
a + :: Orientation p -> Orientation p -> Orientation p
+ Orientation p
b | Orientation p
a forall a. Eq a => a -> a -> Bool
== Orientation p
b = Orientation p
a
        | Bool
otherwise = forall a e. Exception e => e -> a
throw ArithmeticException
NotAddable
  ntimes :: N -> Orientation p -> Orientation p
ntimes N
_ Orientation p
a = Orientation p
a

instance (Additive a, FibredOriented a) => Additive (Op a) where
  zero :: Root (Op a) -> Op a
zero Root (Op a)
r = forall x. x -> Op x
Op (forall a. Additive a => Root a -> a
zero forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Transposable x => x -> x
transpose Root (Op a)
r)
  Op a
a + :: Op a -> Op a -> Op a
+ Op a
b = forall x. x -> Op x
Op (a
a forall a. Additive a => a -> a -> a
+ a
b)
  ntimes :: N -> Op a -> Op a
ntimes N
n (Op a
a) = forall x. x -> Op x
Op (forall a. Additive a => N -> a -> a
ntimes N
n a
a)
  
--------------------------------------------------------------------------------
-- Canonical - Sheaf -

instance Additive a => Projectible a (Sheaf a) where
  prj :: Sheaf a -> a
prj Sheaf a
shf = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Additive a => a -> a -> a
(+) (forall a. Additive a => Root a -> a
zero (forall f. Fibred f => f -> Root f
root Sheaf a
shf)) Sheaf a
shf
  
--------------------------------------------------------------------------------
-- zero' -

-- | the 'zero' to a given root. The type @p c@ serves only as proxy and 'zero'' is
--   lazy in it.
--
--   __Note__ As 'Point' may be a non-injective type family,
--   the type checker needs some times a little bit more information
--   to pic the right 'zero'.
zero' :: Additive a => p a -> Root a -> a
zero' :: forall a (p :: * -> *). Additive a => p a -> Root a -> a
zero' p a
_ = forall a. Additive a => Root a -> a
zero

--------------------------------------------------------------------------------
-- isZero -

-- | check for beeing 'zero'.
isZero :: Additive a => a -> Bool
isZero :: forall a. Additive a => a -> Bool
isZero a
a = a
a forall a. Eq a => a -> a -> Bool
== forall a. Additive a => Root a -> a
zero (forall f. Fibred f => f -> Root f
root a
a)

--------------------------------------------------------------------------------
-- Abelian -

infixl 6 -
-- | 'Additive' structures having for each summand an __/additve inverse/__.
--
--   __Properties__ Let __@a@__ be a 'Additive' structure, then holds:
--  
--  (1) #Abl1#For all @f@ in __@a@__ holds: @'root' ('negate' f) '==' 'root' f@.
--
--  (2) #Abl2#For all @f@ in __@a@__ holds: @f '+' 'negate' f == 'zero' ('root' f)@.
--
--  (3) #Abl3#For all @f@ and @g@ in __@a@__ holds:
--
--      (1) #Abl3_1#If @'root' f '==' 'root' g@ then @f '-' g@ is 'valid' and
--      @'root' (f '-' g) '==' 'root' f@.
--
--      (2) #Abl3_2#If @'root' f '/=' 'root' g@ then @f '-' g@ is not 'valid' and its
--      evaluation will end up in a 'NotAddable'-exception.
--
--  (4) #Abl4#For @f@ and @g@ in __@a@__ with @'root' f '==' 'root' g@ holds:
--   @f '-' g '==' f '+' 'negate' g@.
--
--  (5) #Abl5#For all @z@ in 'Z' and @f@ in __@a@__ holds:
--
--      (1) #Abl5_1#If @0 '<=' z@ then @'ztimes' z f '==' 'ntimes' ('prj' z) f@.
--
--      (2) #Abl5_2#If @z '<' 0@ then  @'ztimes' z f '==' 'negate' ('ntimes' ('prj' z) f)@.
class Additive a => Abelian a where
  {-# MINIMAL negate | (-) #-}

  -- | negation of a summand.
  negate :: a -> a
  negate a
f = forall a. Additive a => Root a -> a
zero (forall f. Fibred f => f -> Root f
root a
f) forall a. Abelian a => a -> a -> a
- a
f

  -- | subtraction of two summands.
  --
  --  __Properties__
  --
  (-) :: a -> a -> a
  a
f - a
g = a
f forall a. Additive a => a -> a -> a
+ forall a. Abelian a => a -> a
negate a
g

  -- | @z@ times of a sumand. 
  ztimes :: Z -> a -> a  
  ztimes Z
z a
f = forall a. Additive a => N -> a -> a
ntimes (forall a b. Projectible a b => b -> a
prj Z
z) a
f' where f' :: a
f' = if Z
z forall a. Ord a => a -> a -> Bool
< Z
0 then forall a. Abelian a => a -> a
negate a
f else a
f

instance Abelian () where
  negate :: () -> ()
negate ()
_ = ()
  ()
_ - :: () -> () -> ()
- ()
_    = ()
  ztimes :: Z -> () -> ()
ztimes Z
_ ()
_ = ()

instance Abelian Int where
  negate :: Int -> Int
negate = forall a. Num a => a -> a
A.negate
  (-)    = forall a. Num a => a -> a -> a
(A.-)
  -- ztimes = error "nyi"

instance Abelian Integer where
  negate :: Integer -> Integer
negate = forall a. Num a => a -> a
A.negate
  (-)    = forall a. Num a => a -> a -> a
(A.-)
  ztimes :: Z -> Integer -> Integer
ztimes Z
z Integer
i = forall a b. Projectible a b => b -> a
prj Z
z forall c. Multiplicative c => c -> c -> c
* Integer
i

instance Abelian Z where
  negate :: Z -> Z
negate = forall a. Num a => a -> a
A.negate
  (-)    = forall a. Num a => a -> a -> a
(A.-)
  ztimes :: Z -> Z -> Z
ztimes = forall c. Multiplicative c => c -> c -> c
(*)
  
instance Abelian Q where
  negate :: Q -> Q
negate = forall a. Num a => a -> a
A.negate
  (-)    = forall a. Num a => a -> a -> a
(A.-)
  ztimes :: Z -> Q -> Q
ztimes Z
z Q
i = forall a b. Embeddable a b => a -> b
inj Z
z forall c. Multiplicative c => c -> c -> c
* Q
i

instance Entity p => Abelian (Orientation p) where
  negate :: Orientation p -> Orientation p
negate = forall x. x -> x
id

instance (Abelian a, FibredOriented a) => Abelian (Op a) where
  negate :: Op a -> Op a
negate (Op a
x) = forall x. x -> Op x
Op (forall a. Abelian a => a -> a
negate a
x)
  Op a
a - :: Op a -> Op a -> Op a
- Op a
b = forall x. x -> Op x
Op (a
aforall a. Abelian a => a -> a -> a
-a
b)
  ztimes :: Z -> Op a -> Op a
ztimes Z
z (Op a
a) = forall x. x -> Op x
Op (forall a. Abelian a => Z -> a -> a
ztimes Z
z a
a)

--------------------------------------------------------------------------------
-- Add -
  
-- | type representing the class of 'Additive' structures.
data Add

type instance Structure Add x = Additive x

instance Transformable Add Typ where tau :: forall x. Struct Add x -> Struct Typ x
tau Struct Add x
Struct = forall s x. Structure s x => Struct s x
Struct
instance Transformable Add Ent where tau :: forall x. Struct Add x -> Struct Ent x
tau Struct Add x
Struct = forall s x. Structure s x => Struct s x
Struct
instance Transformable Add Fbr where tau :: forall x. Struct Add x -> Struct Fbr x
tau Struct Add x
Struct = forall s x. Structure s x => Struct s x
Struct

--------------------------------------------------------------------------------
-- ForgetfulAdd -

-- | transformable to 'Additive' structure.
class (ForgetfulFbr s, Transformable s Add) => ForgetfulAdd s

instance ForgetfulTyp Add
instance ForgetfulFbr Add
instance ForgetfulAdd Add

--------------------------------------------------------------------------------
-- Abl -

-- | type representing the class of 'Abelian' structures.
data Abl

type instance Structure Abl x = Abelian x

instance Transformable Abl Typ where tau :: forall x. Struct Abl x -> Struct Typ x
tau Struct Abl x
Struct = forall s x. Structure s x => Struct s x
Struct
instance Transformable Abl Ent where tau :: forall x. Struct Abl x -> Struct Ent x
tau Struct Abl x
Struct = forall s x. Structure s x => Struct s x
Struct
instance Transformable Abl Fbr where tau :: forall x. Struct Abl x -> Struct Fbr x
tau Struct Abl x
Struct = forall s x. Structure s x => Struct s x
Struct
instance Transformable Abl Add where tau :: forall x. Struct Abl x -> Struct Add x
tau Struct Abl x
Struct = forall s x. Structure s x => Struct s x
Struct

--------------------------------------------------------------------------------
-- ForgetfulAbl -

-- | transformable to 'Abelian' structure.
class (ForgetfulFbr s, ForgetfulAdd s, Transformable s Abl) => ForgetfulAbl s

instance ForgetfulTyp Abl
instance ForgetfulFbr Abl
instance ForgetfulAdd Abl
instance ForgetfulAbl Abl