{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      : OAlg.Structure.Vectorial.Proposition
-- Description : propositions on vectorial structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on 'Vectorial' structures.
module OAlg.Structure.Vectorial.Proposition
  ( -- * Proposition
    prpVec
  , prpVec1, prpVec2, prpVec3, prpVec4, prpVec5, prpVec6, prpVec7

    -- * X
  , XVec(..)
    
    -- ** Direction
  , xoVec
  )
  where

import OAlg.Prelude

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive
import OAlg.Structure.Ring.Definition
import OAlg.Structure.Vectorial.Definition

--------------------------------------------------------------------------------
-- prpVec1 -

-- | validity according to "OAlg.Structure.Vectorial.Definition#Vec1".
prpVec1 :: Vectorial v => X (Scalar v) -> X v -> Statement
prpVec1 :: forall v. Vectorial v => X (Scalar v) -> X v -> Statement
prpVec1 X (Scalar v)
xs X v
xv = String -> Label
Prp String
"Vec1"
  Label -> Statement -> Statement
:<=>: X (Scalar v, v) -> ((Scalar v, v) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Scalar v, v)
xsv
          (\(Scalar v
s,v
v) -> let sv :: v
sv = Scalar v
sScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
v
            in [Statement] -> Statement
And [ v -> Statement
forall a. Validable a => a -> Statement
valid v
sv
                   , (v -> Root v
forall f. Fibred f => f -> Root f
root v
sv Root v -> Root v -> Bool
forall a. Eq a => a -> a -> Bool
== v -> Root v
forall f. Fibred f => f -> Root f
root v
v)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"sv"String -> String -> Parameter
:=(Scalar v, v) -> String
forall a. Show a => a -> String
show (Scalar v
s,v
v)]
                   ]
          )
  where xsv :: X (Scalar v, v)
xsv = X (Scalar v) -> X v -> X (Scalar v, v)
forall a b. X a -> X b -> X (a, b)
xTupple2 X (Scalar v)
xs X v
xv

--------------------------------------------------------------------------------
-- prpVec2 -

-- | validity according to "OAlg.Structure.Vectorial.Definition#Vec2".
prpVec2 :: Vectorial v => X v -> Statement
prpVec2 :: forall v. Vectorial v => X v -> Statement
prpVec2 X v
xv = String -> Label
Prp String
"Vec2"
  Label -> Statement -> Statement
:<=>: X v -> (v -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X v
xv (\v
v -> (Scalar v
forall r. Semiring r => r
rZeroScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== Root v -> v
forall a. Additive a => Root a -> a
zero (v -> Root v
forall f. Fibred f => f -> Root f
root v
v))Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"v"String -> String -> Parameter
:=v -> String
forall a. Show a => a -> String
show v
v])

--------------------------------------------------------------------------------
-- prpVec3 -

-- | validity according to "OAlg.Structure.Vectorial.Definition#Vec3".
prpVec3 :: Vectorial v => p v -> X (Scalar v) -> X (Root v) -> Statement
prpVec3 :: forall v (p :: * -> *).
Vectorial v =>
p v -> X (Scalar v) -> X (Root v) -> Statement
prpVec3 p v
p X (Scalar v)
xs X (Root v)
xr = String -> Label
Prp String
"Vec3"
  Label -> Statement -> Statement
:<=>: X (Scalar v, Root v)
-> ((Scalar v, Root v) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Scalar v, Root v)
xsr
         (\(Scalar v
s,Root v
r) -> let z :: v
z = p v -> Root v -> v
forall a (p :: * -> *). Additive a => p a -> Root a -> a
zero' p v
p Root v
r in (Scalar v
sScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
z v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
z)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"sr"String -> String -> Parameter
:=(Scalar v, Root v) -> String
forall a. Show a => a -> String
show (Scalar v
s,Root v
r)])
  where xsr :: X (Scalar v, Root v)
xsr = X (Scalar v) -> X (Root v) -> X (Scalar v, Root v)
forall a b. X a -> X b -> X (a, b)
xTupple2 X (Scalar v)
xs X (Root v)
xr

--------------------------------------------------------------------------------
-- prpVec4 -

-- | validity according to "OAlg.Structure.Vectorial.Definition#Vec4".
prpVec4 :: Vectorial v => X (Scalar v) -> X v -> Statement
prpVec4 :: forall v. Vectorial v => X (Scalar v) -> X v -> Statement
prpVec4 X (Scalar v)
xs X v
xv = String -> Label
Prp String
"Vec4" Label -> Statement -> Statement
:<=>: X (Scalar v, Scalar v, v)
-> ((Scalar v, Scalar v, v) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Scalar v, Scalar v, v)
xrsv
  (\(Scalar v
r,Scalar v
s,v
v) -> ((Scalar v
r Scalar v -> Scalar v -> Scalar v
forall a. Additive a => a -> a -> a
+ Scalar v
s)Scalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== Scalar v
rScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
v v -> v -> v
forall a. Additive a => a -> a -> a
+ Scalar v
sScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
v)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"rsv"String -> String -> Parameter
:=(Scalar v, Scalar v, v) -> String
forall a. Show a => a -> String
show (Scalar v
r,Scalar v
s,v
v)]
  ) where xrsv :: X (Scalar v, Scalar v, v)
xrsv = X (Scalar v) -> X (Scalar v) -> X v -> X (Scalar v, Scalar v, v)
forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X (Scalar v)
xs X (Scalar v)
xs X v
xv

--------------------------------------------------------------------------------
-- prpVec5 -

-- | validity according to "OAlg.Structure.Vectorial.Definition#Vec5".
prpVec5 :: Vectorial v => X (Scalar v) -> X (Adbl2 v) -> Statement
prpVec5 :: forall v. Vectorial v => X (Scalar v) -> X (Adbl2 v) -> Statement
prpVec5 X (Scalar v)
xs X (Adbl2 v)
xa2 = String -> Label
Prp String
"Vec5" Label -> Statement -> Statement
:<=>: X (Scalar v, Adbl2 v)
-> ((Scalar v, Adbl2 v) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Scalar v, Adbl2 v)
xsa2
  (\(Scalar v
s,Adbl2 v
v v
w) -> (Scalar v
sScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!(v
v v -> v -> v
forall a. Additive a => a -> a -> a
+ v
w) v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== Scalar v
sScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
v v -> v -> v
forall a. Additive a => a -> a -> a
+ Scalar v
sScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
w)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"svw"String -> String -> Parameter
:=(Scalar v, v, v) -> String
forall a. Show a => a -> String
show (Scalar v
s,v
v,v
w)])
  where xsa2 :: X (Scalar v, Adbl2 v)
xsa2 = X (Scalar v) -> X (Adbl2 v) -> X (Scalar v, Adbl2 v)
forall a b. X a -> X b -> X (a, b)
xTupple2 X (Scalar v)
xs X (Adbl2 v)
xa2

--------------------------------------------------------------------------------
-- prpVec6 -

-- | validity according to "OAlg.Structure.Vectorial.Definition#Vec6".
prpVec6 :: Vectorial v => X v -> Statement
prpVec6 :: forall v. Vectorial v => X v -> Statement
prpVec6 X v
xv = String -> Label
Prp String
"Vec6" Label -> Statement -> Statement
:<=>: X v -> (v -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X v
xv (\v
v -> (Scalar v
forall r. Semiring r => r
rOneScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"v"String -> String -> Parameter
:=v -> String
forall a. Show a => a -> String
show v
v])

--------------------------------------------------------------------------------
-- prpVec7 -

-- | validity according to "OAlg.Structure.Vectorial.Definition#Vec7".
prpVec7 :: Vectorial v => X (Scalar v) -> X v -> Statement
prpVec7 :: forall v. Vectorial v => X (Scalar v) -> X v -> Statement
prpVec7 X (Scalar v)
xs X v
xv = String -> Label
Prp String
"Vec7" Label -> Statement -> Statement
:<=>: X (Scalar v, Scalar v, v)
-> ((Scalar v, Scalar v, v) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Scalar v, Scalar v, v)
xrsv
  (\(Scalar v
r,Scalar v
s,v
v) -> ((Scalar v
rScalar v -> Scalar v -> Scalar v
forall c. Multiplicative c => c -> c -> c
*Scalar v
s)Scalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== Scalar v
rScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!(Scalar v
sScalar v -> v -> v
forall v. Vectorial v => Scalar v -> v -> v
!v
v)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"rsv"String -> String -> Parameter
:=(Scalar v, Scalar v, v) -> String
forall a. Show a => a -> String
show (Scalar v
r,Scalar v
s,v
v)])
  where xrsv :: X (Scalar v, Scalar v, v)
xrsv = X (Scalar v) -> X (Scalar v) -> X v -> X (Scalar v, Scalar v, v)
forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X (Scalar v)
xs X (Scalar v)
xs X v
xv

--------------------------------------------------------------------------------
-- XVec -

-- | random variable to validate 'Vectorial' structures.
data XVec v = XVec (X (Scalar v)) (X (Root v)) (X v) (X (Adbl2 v))

instance Vectorial v => Validable (XVec v) where
  valid :: XVec v -> Statement
valid (XVec X (Scalar v)
xs X (Root v)
xr X v
xv X (Adbl2 v)
xa2)
    = [Statement] -> Statement
And [ X (Scalar v) -> Statement
forall a. Validable a => a -> Statement
valid X (Scalar v)
xs
          , X (Root v) -> Statement
forall a. Validable a => a -> Statement
valid X (Root v)
xr
          , X v -> Statement
forall a. Validable a => a -> Statement
valid X v
xv
          , X (Adbl2 v) -> Statement
forall a. Validable a => a -> Statement
valid X (Adbl2 v)
xa2
          ]

--------------------------------------------------------------------------------
-- prpVec -

-- | validity of the 'Vectorial' structure of @__v__@.
prpVec :: Vectorial v => XVec v -> Statement
prpVec :: forall v. Vectorial v => XVec v -> Statement
prpVec (XVec X (Scalar v)
xs X (Root v)
xr X v
xv X (Adbl2 v)
xa2) = String -> Label
Prp String
"Vec" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ X (Scalar v) -> X v -> Statement
forall v. Vectorial v => X (Scalar v) -> X v -> Statement
prpVec1 X (Scalar v)
xs X v
xv
      , X v -> Statement
forall v. Vectorial v => X v -> Statement
prpVec2 X v
xv
      , X v -> X (Scalar v) -> X (Root v) -> Statement
forall v (p :: * -> *).
Vectorial v =>
p v -> X (Scalar v) -> X (Root v) -> Statement
prpVec3 X v
xv X (Scalar v)
xs X (Root v)
xr
      , X (Scalar v) -> X v -> Statement
forall v. Vectorial v => X (Scalar v) -> X v -> Statement
prpVec4 X (Scalar v)
xs X v
xv
      , X (Scalar v) -> X (Adbl2 v) -> Statement
forall v. Vectorial v => X (Scalar v) -> X (Adbl2 v) -> Statement
prpVec5 X (Scalar v)
xs X (Adbl2 v)
xa2
      , X v -> Statement
forall v. Vectorial v => X v -> Statement
prpVec6 X v
xv
      , X (Scalar v) -> X v -> Statement
forall v. Vectorial v => X (Scalar v) -> X v -> Statement
prpVec7 X (Scalar v)
xs X v
xv
      ]


--------------------------------------------------------------------------------
-- xodVec -

-- | the induced random variable.
xoVec :: FibredOriented v => X (Scalar v) -> XOrtOrientation v -> XVec v
xoVec :: forall v.
FibredOriented v =>
X (Scalar v) -> XOrtOrientation v -> XVec v
xoVec X (Scalar v)
xs XOrtOrientation v
xo = X (Scalar v) -> X (Root v) -> X v -> X (Adbl2 v) -> XVec v
forall v.
X (Scalar v) -> X (Root v) -> X v -> X (Adbl2 v) -> XVec v
XVec X (Scalar v)
xs X (Root v)
xr X v
xv X (Adbl2 v)
xa2 where
  xr :: X (Root v)
xr = XOrtOrientation v -> X (Root v)
forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot XOrtOrientation v
xo
  xv :: X v
xv = XOrtOrientation v -> X v
forall f. XOrtOrientation f -> XFbr f
xoFbr XOrtOrientation v
xo
  xa2 :: X (Adbl2 v)
xa2 = XOrtOrientation v -> X (Adbl2 v)
forall a. FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
xoAdbl2 XOrtOrientation v
xo