{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneKindSignatures #-}

-- |
-- Module      : OAlg.Structure.Vectorial.Definition
-- Description : definition of vectorial structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- definition of vectorial structures, i.e. 'Additive' structures with a scalar multiplication @('!')@.
module OAlg.Structure.Vectorial.Definition
  ( -- * Vectorial
    Vectorial(..), Vec, ForgetfulVec

    -- * Euclidean
  , Euclidean(..)
  )
  where

import Control.Exception

import OAlg.Prelude

import OAlg.Structure.Exception
import OAlg.Structure.Oriented.Definition(Orientation(..))
import OAlg.Structure.Multiplicative.Definition
import OAlg.Structure.Fibred.Definition
import OAlg.Structure.Additive.Definition
import OAlg.Structure.Ring.Definition
import OAlg.Structure.Number.Definition


--------------------------------------------------------------------------------
-- Vectorial -

infixr 8 !

-- | 'Additive' structures with a __total__ defined __scalar multiplication__ from the left
--   by a __commutative semi ring__. The entities of __@v@__ are called __vector__.
--
-- __Properties__ Let __@v@__ b a 'Vectorial' structure, then holds:
--
-- (1) #Vec1#For all @s@ in @'Scalar' __v__@ and @v@ in __@v@__ holds:
-- @s'!'v@ is 'valid' and @'root' (s'!'v) '==' 'root' v@.
--
-- (2) #Vec2#For all @v@ in __@v@__ holds: @0'!'v '==' 'zero' ('root' v)@.
--
-- (3) #Vec3#For all @s@ in @'Scalar' __v__@ and @r@ in @'Root' __v__@ holds
-- @s'!''zero' r '==' 'zero' r@.
--
-- (4) #Vec4#For all @r@, @s@ in @'Scalar' __v__@ and @v@ in __@v@__ holds:
-- @(r '+' s)'!'v '==' r'!'v '+' s'!'v@.
--
-- (5) #Vec5#For all @s@ in @'Scalar' __v__@ and @v@, @w@ in __@v@__ with
-- @'root' v '==' 'root' w@ holds: @s'!'(v '+' w) '==' s'!'v '+' s'!'w@.
--
-- (6) #Vec6#For all @v@ in __@v@__ holds: @1'!'v '==' v@.
--
-- (7) #Vec7#For all @r@, @s@ in @'Scalar' __v__@ and @v@ in __@v@__ holds:
-- @(r'*'s)'!'v '==' r'!'(s'!'v)@.
class (Semiring (Scalar v), Commutative (Scalar v), Additive v) => Vectorial v where
  -- | the type of scalars.
  type Scalar v

  -- | scalar multiplication of a vector.
  (!) :: Scalar v -> v -> v

instance Vectorial () where
  type Scalar () = Q
  ! :: Scalar () -> () -> ()
(!) = forall a. Acyclic a => Q -> a -> a
qtimes

instance Vectorial Int where
  type Scalar Int = Int
  ! :: Scalar Int -> Int -> Int
(!) = forall c. Multiplicative c => c -> c -> c
(*)

instance Vectorial Integer where
  type Scalar Integer = Integer
  ! :: Scalar Integer -> Integer -> Integer
(!) = forall c. Multiplicative c => c -> c -> c
(*)

instance Vectorial N where
  type Scalar N = N
  ! :: Scalar N -> N -> N
(!) = forall c. Multiplicative c => c -> c -> c
(*)

instance Vectorial Z where
  type Scalar Z = Z
  ! :: Scalar Z -> Z -> Z
(!) = forall c. Multiplicative c => c -> c -> c
(*)

instance Vectorial Q where
  type Scalar Q = Q
  ! :: Scalar Q -> Q -> Q
(!) = forall c. Multiplicative c => c -> c -> c
(*)

instance Entity p => Vectorial (Orientation p) where
  type Scalar (Orientation p) = Q
  Scalar (Orientation p)
_ ! :: Scalar (Orientation p) -> Orientation p -> Orientation p
! Orientation p
o = Orientation p
o

instance (Vectorial v, FibredOriented v) => Vectorial (Op v) where
  type Scalar (Op v) = Scalar v
  Scalar (Op v)
s ! :: Scalar (Op v) -> Op v -> Op v
! (Op v
v) = forall x. x -> Op x
Op (Scalar (Op v)
sforall v. Vectorial v => Scalar v -> v -> v
!v
v)
  
--------------------------------------------------------------------------------
-- Euclidean -
infix 7 <!>
  
-- | 'Vectorial' structures with a __partially__ defined scalar product.
--
-- __Properties__ 
--
-- (1) For all @v@, @w@ holds: if @'root' v '==' 'root' w@ then @v '<!>' w@ is 'valid', otherwise
-- a 'UndefinedScalarproduct'-exception will be thrown.
--
-- (2) For all @u@ holds: @u '<!>' 'zero' ('root' u) '==' 'rZero'@.
--
-- (3) For all @u@, @v@ and @w@ with @'root' u '==' 'root' w@ and
-- @'root' w '==' 'root' v  @
-- holds: @u '<!>' (v '+' w) '==' u '<!>' v '+' u '<!>' w@.
--
-- (4) For all @w@ holds: @'zero' ('root' w) '<!>' w '==' 'rZero'@.
--
-- (5) For all @u@, @v@ and @w@ with @'root' w '==' 'root' u@ and
-- @'root' u '==' 'root' v  @
-- holds: @(u '+' v) '<!>' w '==' u '<!>' w '+' v' <!>' w@.
class Vectorial v => Euclidean v where

  -- | the scalar product of two vectors.
  (<!>) :: v -> v -> Scalar v

instance Euclidean N where
  <!> :: N -> N -> Scalar N
(<!>) = forall c. Multiplicative c => c -> c -> c
(*)

instance Euclidean Z where
  <!> :: Z -> Z -> Scalar Z
(<!>) = forall c. Multiplicative c => c -> c -> c
(*)

instance Euclidean Q where
  <!> :: Q -> Q -> Scalar Q
(<!>) = forall c. Multiplicative c => c -> c -> c
(*)

instance Entity p => Euclidean (Orientation p) where
  Orientation p
a <!> :: Orientation p -> Orientation p -> Scalar (Orientation p)
<!> Orientation p
b | forall f. Fibred f => f -> Root f
root Orientation p
a forall a. Eq a => a -> a -> Bool
== forall f. Fibred f => f -> Root f
root Orientation p
b = Q
0
          | Bool
otherwise        = forall a e. Exception e => e -> a
throw ArithmeticException
UndefinedScalarproduct
          

--------------------------------------------------------------------------------
-- Vec -
  
-- | type representing the class of @__k__-'Vectorial'@ structures.
data Vec k

type instance Structure (Vec k) x = (Vectorial x, k ~ Scalar x)

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

--------------------------------------------------------------------------------
-- ForgetfulVec -

-- | transformable to @__k__-'Vectorial'@ structure.
class ( ForgetfulFbr (s k), ForgetfulAdd (s k)
      , Transformable (s k) (Vec k)
      ) => ForgetfulVec k s

instance ForgetfulTyp (Vec k)
instance ForgetfulFbr (Vec k)
instance ForgetfulAdd (Vec k)
instance ForgetfulVec k Vec