{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DataKinds #-}

-- |
-- Module      : OAlg.Entity.Matrix.Proposition
-- Description : propositions on matrices
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on matrices.
module OAlg.Entity.Matrix.Proposition
  (
    -- * Proposition
    prpMatrix, prpMatrixZ
    
  ) where

import OAlg.Prelude

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.Additive
import OAlg.Structure.Vectorial
import OAlg.Structure.Distributive
import OAlg.Structure.Algebraic

import OAlg.Limes.ProductsAndSums

import OAlg.Entity.Natural

import OAlg.Entity.Matrix.Definition
import OAlg.Entity.Matrix.ProductsAndSums

--------------------------------------------------------------------------------
-- prpMatrix -

-- | validity of the algebraic structure of matrices.
prpMatrix :: Distributive x
  => XOrtOrientation (Matrix x)
  -> XOrtSite From (Matrix x)
  -> XOrtSite To (Matrix x)
  -> Statement
prpMatrix :: forall x.
Distributive x =>
XOrtOrientation (Matrix x)
-> XOrtSite 'From (Matrix x)
-> XOrtSite 'To (Matrix x)
-> Statement
prpMatrix XOrtOrientation (Matrix x)
xo XOrtSite 'From (Matrix x)
xf XOrtSite 'To (Matrix x)
xt = String -> Label
Prp String
"Matrix" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ forall q. Oriented q => XOrt q -> Statement
prpOrt (forall q. XOrtOrientation q -> XOrt q
xoOrt XOrtOrientation (Matrix x)
xo)
      , forall c. Multiplicative c => XMlt c -> Statement
prpMlt (forall c. Multiplicative c => X N -> XOrtOrientation c -> XMlt c
xoMlt (N -> N -> X N
xNB N
0 N
10) XOrtOrientation (Matrix x)
xo)
      , forall f. Fibred f => XFbr f -> Statement
prpFbr (forall q. XOrtOrientation q -> XOrt q
xoFbr XOrtOrientation (Matrix x)
xo)
      , forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (forall q. XOrtOrientation q -> XOrt q
xoFbrOrt XOrtOrientation (Matrix x)
xo)
      , forall a. Additive a => XAdd a -> Statement
prpAdd (forall a. FibredOriented a => X N -> XOrtOrientation a -> XAdd a
xoAdd (N -> N -> X N
xNB N
0 N
5) XOrtOrientation (Matrix x)
xo)
      , forall d. Distributive d => XDst d -> Statement
prpDst (forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'From d -> XOrtSite 'To d -> XDst d
xoDst XOrtOrientation (Matrix x)
xo XOrtSite 'From (Matrix x)
xf XOrtSite 'To (Matrix x)
xt)
      ]


dstMatrix :: Int -> X (Matrix x) -> IO ()
dstMatrix :: forall x. Int -> X (Matrix x) -> IO ()
dstMatrix = forall x. (x -> [String]) -> Int -> X x -> IO ()
putDstr (\Matrix x
m -> [forall {x}. Matrix x -> String
rws Matrix x
m,forall {x}. Matrix x -> String
cls Matrix x
m]) where
  rws :: Matrix x -> String
rws (Matrix Dim x (Point x)
r Dim x (Point x)
_ Entries N N x
_) = forall a. Show a => a -> String
show forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. LengthN x => x -> N
lengthN Dim x (Point x)
r
  cls :: Matrix x -> String
cls (Matrix Dim x (Point x)
_ Dim x (Point x)
c Entries N N x
_) = forall a. Show a => a -> String
show forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. LengthN x => x -> N
lengthN Dim x (Point x)
c


--------------------------------------------------------------------------------
-- prpMatrixZ -

-- | validity of the algebraic structure of block matrices of 'Z'.
prpMatrixZ :: Statement
prpMatrixZ :: Statement
prpMatrixZ = String -> Label
Prp String
"MatrixZ"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall x.
Distributive x =>
XOrtOrientation (Matrix x)
-> XOrtSite 'From (Matrix x)
-> XOrtSite 'To (Matrix x)
-> Statement
prpMatrix XOrtOrientation (Matrix (Matrix Z))
xo XOrtSite 'From (Matrix (Matrix Z))
xf XOrtSite 'To (Matrix (Matrix Z))
xt
            , forall a. Abelian a => XAbl a -> Statement
prpAbl (forall a. FibredOriented a => X Z -> XOrtOrientation a -> XAbl a
xoAbl (Z -> Z -> X Z
xZB (-Z
10) Z
10) XOrtOrientation (Matrix (Matrix Z))
xo)            
            , forall v. Vectorial v => XVec v -> Statement
prpVec (forall v.
FibredOriented v =>
X (Scalar v) -> XOrtOrientation v -> XVec v
xoVec X Z
xZ XOrtOrientation (Matrix (Matrix Z))
xo)
            , forall a. Algebraic a => XAlg a -> Statement
prpAlg (forall a (d :: Site).
Algebraic a =>
X (Scalar a) -> XOrtSite d a -> XAlg a
xoAlg X Z
xZ XOrtSite 'From (Matrix (Matrix Z))
xf)
            , String -> Label
Label String
"Sums N3 (Matrix Z)" 
                 Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid (forall x (n :: N'). Distributive x => Sums n (Matrix x)
mtxSums :: Sums N3 (Matrix Z))
            ]
  where xo :: XOrtOrientation (Matrix (Matrix Z))
xo = XOrtOrientation (Matrix (Matrix Z))
xodZZ
        xf :: XOrtSite 'From (Matrix (Matrix Z))
xf = forall q. Oriented q => XOrtOrientation q -> XOrtSite 'From q
xoFrom XOrtOrientation (Matrix (Matrix Z))
xo
        xt :: XOrtSite 'To (Matrix (Matrix Z))
xt = forall q. Oriented q => XOrtOrientation q -> XOrtSite 'To q
xoTo XOrtOrientation (Matrix (Matrix Z))
xo