{-# 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, TransformableAdd, tauAdd

    -- * Abelian

  , Abelian(..), isZero, Abl, TransformableAbl

  -- * X

  , xSheaf, xSheafRoot
  )
  where

import qualified Prelude as A

import Control.Monad
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.Oriented.Opposite
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred.Definition
import OAlg.Structure.FibredOriented

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

-- 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 = (a -> a -> a) -> a -> [a] -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> a -> a
forall a. Additive a => a -> a -> a
(+) (Root a -> a
forall a. Additive a => Root a -> a
zero (a -> Root a
forall f. Fibred f => f -> Root f
root a
f)) ([a] -> a) -> [a] -> a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> [a] -> [a]
forall a. N -> [a] -> [a]
takeN N
n ([a] -> [a]) -> [a] -> [a]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ a -> [a]
forall a. a -> [a]
repeat (a -> [a]) -> a -> [a]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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
(+) = 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
(+) = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(A.+)
  ntimes :: N -> Integer -> Integer
ntimes N
n Integer
z = N -> Integer
forall a b. Embeddable a b => a -> b
inj N
n Integer -> Integer -> Integer
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
(+) = N -> N -> N
forall a. Num a => a -> a -> a
(A.+)
  ntimes :: N -> N -> N
ntimes = N -> N -> N
forall c. Multiplicative c => c -> c -> c
(*)

instance Additive Z where
  zero :: Root Z -> Z
zero Root Z
_ = Z
0
  + :: Z -> Z -> Z
(+) = Z -> Z -> Z
forall a. Num a => a -> a -> a
(A.+)
  ntimes :: N -> Z -> Z
ntimes N
n Z
z = N -> Z
forall a b. Embeddable a b => a -> b
inj N
n Z -> Z -> Z
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
(+) = Q -> Q -> Q
forall a. Num a => a -> a -> a
(A.+)
  ntimes :: N -> Q -> Q
ntimes N
n Q
q = N -> Q
forall a b. Embeddable a b => a -> b
inj N
n Q -> Q -> Q
forall c. Multiplicative c => c -> c -> c
* Q
q

instance Entity p => Additive (Orientation p) where
  zero :: Root (Orientation p) -> Orientation p
zero = Orientation p -> Orientation p
Root (Orientation p) -> Orientation p
forall x. x -> x
id
  Orientation p
a + :: Orientation p -> Orientation p -> Orientation p
+ Orientation p
b | Orientation p
a Orientation p -> Orientation p -> Bool
forall a. Eq a => a -> a -> Bool
== Orientation p
b = Orientation p
a
        | Bool
otherwise = ArithmeticException -> Orientation p
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 => Additive (Id a) where
  zero :: Root (Id a) -> Id a
zero Root (Id a)
r = a -> Id a
forall x. x -> Id x
Id (Root a -> a
forall a. Additive a => Root a -> a
zero Root a
Root (Id a)
r)
  Id a
a + :: Id a -> Id a -> Id a
+ Id a
b = a -> Id a
forall x. x -> Id x
Id (a
aa -> a -> a
forall a. Additive a => a -> a -> a
+a
b)
  ntimes :: N -> Id a -> Id a
ntimes N
n (Id a
a) = a -> Id a
forall x. x -> Id x
Id (N -> a -> a
forall a. Additive a => N -> a -> a
ntimes N
n a
a)
  
instance (Additive a, FibredOriented a) => Additive (Op a) where
  zero :: Root (Op a) -> Op a
zero Root (Op a)
r = a -> Op a
forall x. x -> Op x
Op (Orientation (Point a) -> a
Root a -> a
forall a. Additive a => Root a -> a
zero (Orientation (Point a) -> a) -> Orientation (Point a) -> a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Orientation (Point a) -> Orientation (Point a)
forall x. Transposable x => x -> x
transpose Orientation (Point a)
Root (Op a)
r)
  Op a
a + :: Op a -> Op a -> Op a
+ Op a
b = a -> Op a
forall x. x -> Op x
Op (a
b a -> a -> a
forall a. Additive a => a -> a -> a
+ a
a)
  ntimes :: N -> Op a -> Op a
ntimes N
n (Op a
a) = a -> Op a
forall x. x -> Op x
Op (N -> a -> a
forall a. Additive a => N -> a -> a
ntimes N
n a
a)

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

-- 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
_ = Root a -> 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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Root a -> a
forall a. Additive a => Root a -> a
zero (a -> Root a
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 = Root a -> a
forall a. Additive a => Root a -> a
zero (a -> Root a
forall f. Fibred f => f -> Root f
root a
f) a -> a -> a
forall a. Abelian a => a -> a -> a
- a
f

  -- | subtraction of two summands.

  --

  --  __Properties__

  --

  (-) :: a -> a -> a
  a
f - a
g = a
f a -> a -> a
forall a. Additive a => a -> 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 = N -> a -> a
forall a. Additive a => N -> a -> a
ntimes (Z -> N
forall a b. Projectible a b => b -> a
prj Z
z) a
f' where f' :: a
f' = if Z
z Z -> Z -> Bool
forall a. Ord a => a -> a -> Bool
< Z
0 then a -> a
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 = Int -> Int
forall a. Num a => a -> a
A.negate
  (-)    = Int -> Int -> Int
forall a. Num a => a -> a -> a
(A.-)
  -- ztimes = error "nyi"


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

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

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

instance (Abelian a, FibredOriented a) => Abelian (Op a) where
  negate :: Op a -> Op a
negate (Op a
x) = a -> Op a
forall x. x -> Op x
Op (a -> a
forall a. Abelian a => a -> a
negate a
x)
  Op a
a - :: Op a -> Op a -> Op a
- Op a
b = a -> Op a
forall x. x -> Op x
Op (a
aa -> a -> a
forall a. Abelian a => a -> a -> a
-a
b)
  ztimes :: Z -> Op a -> Op a
ztimes Z
z (Op a
a) = a -> Op a
forall x. x -> Op x
Op (Z -> a -> a
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 = Struct Typ x
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 = Struct Ent x
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 = Struct Fbr x
forall s x. Structure s x => Struct s x
Struct

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

-- tauAdd -


-- | 'tau' for 'Add'.

tauAdd :: Transformable s Add => Struct s x -> Struct Add x
tauAdd :: forall s x. Transformable s Add => Struct s x -> Struct Add x
tauAdd = Struct s x -> Struct Add x
forall x. Struct s x -> Struct Add x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau

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

-- TransformableAdd -


-- | helper class to avoid undecidable instances.

class (TransformableFbr s, Transformable s Add) => TransformableAdd s

instance TransformableTyp Add
instance TransformableFbr Add
instance TransformableAdd 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 = Struct Typ x
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 = Struct Ent x
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 = Struct Fbr x
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 = Struct Add x
forall s x. Structure s x => Struct s x
Struct

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

-- TransformableAbl -


-- | transformable to 'Abelian' structure.

class (Transformable s Fbr, Transformable s Add, Transformable s Abl) => TransformableAbl s

instance TransformableTyp Abl
instance TransformableFbr Abl
instance TransformableAdd Abl
instance TransformableAbl Abl

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

-- adjZero -


-- | adjoins a 'zero' stalk for empty 'root's.

adjZero :: Additive a => XStalk a -> XStalk a
adjZero :: forall a. Additive a => XStalk a -> XStalk a
adjZero (XStalk X (Root a)
xr Root a -> X a
xrs) = X (Root a) -> (Root a -> X a) -> XStalk a
forall x. X (Root x) -> (Root x -> X x) -> XStalk x
XStalk X (Root a)
xr Root a -> X a
xrs' where
  xrs' :: Root a -> X a
xrs' Root a
r = case Root a -> X a
xrs Root a
r of
    X a
XEmpty -> a -> X a
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Root a -> a
forall a. Additive a => Root a -> a
zero Root a
r)
    X a
xs     -> X a
xs

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

-- xSheafRoot -


-- | random variable of sheafs, all based on the given 'root' and with the given length.

xSheafRoot :: Additive a => XStalk a -> N -> Root a -> X (Sheaf a)
xSheafRoot :: forall a. Additive a => XStalk a -> N -> Root a -> X (Sheaf a)
xSheafRoot XStalk a
xs = XStalk a -> N -> Root a -> X (Sheaf a)
forall f. Fibred f => XStalk f -> N -> Root f -> X (Sheaf f)
xSheafRootMax (XStalk a -> XStalk a
forall a. Additive a => XStalk a -> XStalk a
adjZero XStalk a
xs)

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

-- xSheaf -


-- | random variable of sheafs with the given length.

xSheaf :: Additive a => XStalk a -> N -> X (Sheaf a)
xSheaf :: forall a. Additive a => XStalk a -> N -> X (Sheaf a)
xSheaf XStalk a
xs = XStalk a -> N -> X (Sheaf a)
forall f. Fibred f => XStalk f -> N -> X (Sheaf f)
xSheafMax (XStalk a -> XStalk a
forall a. Additive a => XStalk a -> XStalk a
adjZero XStalk a
xs)