{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      : OAlg.Structure.Algebraic.Proposition
-- Description : propositions on algebraic structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on 'Algebraic' structures.
module OAlg.Structure.Algebraic.Proposition
  ( -- * Proposition
    prpAlg, prpAlg1

    -- * X
  , XAlg(..)

    -- ** Direction
  , xoAlg
  )
  where

import OAlg.Prelude

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Vectorial.Definition
import OAlg.Structure.Algebraic.Definition

--------------------------------------------------------------------------------
-- prpAlg1 -

-- | validity according to "OAlg.Structure.Algebraic.Definition#Alg1".
prpAlg1 :: Algebraic a => X (Scalar a) -> X (Mltp2 a) -> Statement
prpAlg1 :: forall a. Algebraic a => X (Scalar a) -> X (Mltp2 a) -> Statement
prpAlg1 X (Scalar a)
xs X (Mltp2 a)
xm2 = String -> Label
Prp String
"Alg1" Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (Scalar a, Mltp2 a)
xsab
  (\(Scalar a
r,Mltp2 a
a a
b)
   -> let rab :: a
rab = Scalar a
rforall v. Vectorial v => Scalar v -> v -> v
!(a
aforall c. Multiplicative c => c -> c -> c
*a
b)
       in [Statement] -> Statement
And [ (a
rab forall a. Eq a => a -> a -> Bool
== (Scalar a
rforall v. Vectorial v => Scalar v -> v -> v
!a
a)forall c. Multiplicative c => c -> c -> c
*a
b)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"rab"String -> String -> Parameter
:=forall a. Show a => a -> String
show (Scalar a
r,a
a,a
b)]
              , (a
rab forall a. Eq a => a -> a -> Bool
== a
aforall c. Multiplicative c => c -> c -> c
*(Scalar a
rforall v. Vectorial v => Scalar v -> v -> v
!a
b))Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"rab"String -> String -> Parameter
:=forall a. Show a => a -> String
show (Scalar a
r,a
a,a
b)]
              ]
  ) where xsab :: X (Scalar a, Mltp2 a)
xsab = forall a b. X a -> X b -> X (a, b)
xTupple2 X (Scalar a)
xs X (Mltp2 a)
xm2

--------------------------------------------------------------------------------
-- XAlg -

-- | random variable to validate 'Algebraic' structures.
data XAlg a = XAlg (X (Scalar a)) (X (Mltp2 a))

instance Algebraic a => Validable (XAlg a) where
  valid :: XAlg a -> Statement
valid (XAlg X (Scalar a)
xs X (Mltp2 a)
xm2) = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid X (Scalar a)
xs
                            , forall a. Validable a => a -> Statement
valid X (Mltp2 a)
xm2
                            ]

-----------------------------------------------------------------------------------------
-- prpAlg -

-- | validity of the 'Algebraic' structure of __@a@__.
prpAlg :: Algebraic a => XAlg a -> Statement
prpAlg :: forall a. Algebraic a => XAlg a -> Statement
prpAlg (XAlg X (Scalar a)
xs X (Mltp2 a)
xm2) = String -> Label
Prp String
"Alg"
  Label -> Statement -> Statement
:<=>: forall a. Algebraic a => X (Scalar a) -> X (Mltp2 a) -> Statement
prpAlg1 X (Scalar a)
xs X (Mltp2 a)
xm2


--------------------------------------------------------------------------------
-- xoAlg -

-- | the induces random variable.
xoAlg :: Algebraic a => X (Scalar a) -> XOrtSite d a -> XAlg a
xoAlg :: forall a (d :: Site).
Algebraic a =>
X (Scalar a) -> XOrtSite d a -> XAlg a
xoAlg X (Scalar a)
xs XOrtSite d a
xsite = forall a. X (Scalar a) -> X (Mltp2 a) -> XAlg a
XAlg X (Scalar a)
xs (forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp2 c)
xMltp2 XOrtSite d a
xsite)