{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}

-- |
-- Module      : OAlg.Entity.Matrix.ProductsAndSums
-- Description : products and sums for matrices
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- 'Products' and 'Sums' for matrices.
module OAlg.Entity.Matrix.ProductsAndSums
  ( mtxProducts, mtxSums
  ) where

import Control.Monad

import Data.Foldable
import Data.List (map)

import OAlg.Prelude

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Distributive

import OAlg.Hom.Oriented

import OAlg.Entity.FinList
import OAlg.Entity.Diagram
import OAlg.Entity.Sequence.PSequence

import OAlg.Limes.Cone
import OAlg.Limes.Definition
import OAlg.Limes.Limits
import OAlg.Limes.ProductsAndSums

import OAlg.Entity.Matrix.Dim
import OAlg.Entity.Matrix.Definition
import OAlg.Entity.Matrix.Entries

--------------------------------------------------------------------------------
-- mtxProducts -

-- | products for matrices.
mtxProducts :: Distributive x => Products n (Matrix x)
mtxProducts :: forall x (n :: N'). Distributive x => Products n (Matrix x)
mtxProducts = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits forall x (n :: N').
Distributive x =>
ProductDiagram n (Matrix x) -> Product n (Matrix x)
prd where
  
  prd :: Distributive x => ProductDiagram n (Matrix x) -> Product n (Matrix x)
  prd :: forall x (n :: N').
Distributive x =>
ProductDiagram n (Matrix x) -> Product n (Matrix x)
prd ProductDiagram n (Matrix x)
d = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective ProductCone n (Matrix x)
l forall {n :: N'}. ProductCone n (Matrix x) -> Matrix x
u where
    l :: ProductCone n (Matrix x)
l = forall x (n :: N').
Distributive x =>
ProductDiagram n (Matrix x) -> ProductCone n (Matrix x)
lim ProductDiagram n (Matrix x)
d
    u :: ProductCone n (Matrix x) -> Matrix x
u = forall x (n :: N').
Distributive x =>
ProductCone n (Matrix x) -> Matrix x
univ

  lim :: Distributive x => ProductDiagram n (Matrix x) -> ProductCone n (Matrix x)
  lim :: forall x (n :: N').
Distributive x =>
ProductDiagram n (Matrix x) -> ProductCone n (Matrix x)
lim d :: ProductDiagram n (Matrix x)
d@(DiagramDiscrete FinList n (Point (Matrix x))
ps)  = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective ProductDiagram n (Matrix x)
d Dim x (Point x)
l (forall x (n :: N').
Distributive x =>
N
-> Dim x (Point x)
-> FinList n (Dim x (Point x))
-> FinList n (Matrix x)
prjs N
0 Dim x (Point x)
l FinList n (Point (Matrix x))
ps) where
    l :: Dim x (Point x)
l = forall x. Oriented x => Dim' (Matrix x) -> Dim' x
mtxJoinDim forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall p x. (Entity p, p ~ Point x) => [p] -> Dim x p
productDim forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList FinList n (Point (Matrix x))
ps

    prjs :: Distributive x
      => N -> Dim x (Point x) -> FinList n (Dim x (Point x)) -> FinList n (Matrix x)
    prjs :: forall x (n :: N').
Distributive x =>
N
-> Dim x (Point x)
-> FinList n (Dim x (Point x))
-> FinList n (Matrix x)
prjs N
_ Dim x (Point x)
_ FinList n (Dim x (Point x))
Nil     = forall a. FinList N0 a
Nil
    prjs N
j Dim x (Point x)
l (Dim x (Point x)
r:|FinList n (Dim x (Point x))
rs) = forall {x}.
(Additive x, Multiplicative x) =>
N -> Dim x (Point x) -> Dim x (Point x) -> Matrix x
prj N
j Dim x (Point x)
l Dim x (Point x)
r forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| forall x (n :: N').
Distributive x =>
N
-> Dim x (Point x)
-> FinList n (Dim x (Point x))
-> FinList n (Matrix x)
prjs (N
jforall a. Additive a => a -> a -> a
+N
rl) Dim x (Point x)
l FinList n (Dim x (Point x))
rs where
      rl :: N
rl = forall x. LengthN x => x -> N
lengthN Dim x (Point x)
r

    prj :: N -> Dim x (Point x) -> Dim x (Point x) -> Matrix x
prj N
j Dim x (Point x)
l Dim x (Point x)
r = forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim x (Point x)
r Dim x (Point x)
l Entries N N x
os where
      os :: Entries N N x
os = forall x i j. Additive x => Entries i j x -> Entries i j x
etsElimZeros forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i j x. PSequence (i, j) x -> Entries i j x
Entries forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Point x
p,N
i) -> (forall c. Multiplicative c => Point c -> c
one Point x
p,(N
i,N
iforall a. Additive a => a -> a -> a
+N
j))) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall p x. (p ~ Point x) => Dim x p -> [(p, N)]
dimxs Dim x (Point x)
r

  univ :: Distributive x
    => ProductCone n (Matrix x) -> Matrix x
  univ :: forall x (n :: N').
Distributive x =>
ProductCone n (Matrix x) -> Matrix x
univ (ConeProjective Diagram 'Discrete n N0 (Matrix x)
_ Point (Matrix x)
t FinList n (Matrix x)
cs)
    = forall x. Oriented x => Matrix (Matrix x) -> Matrix x
mtxJoin forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim (Matrix x) (Point (Matrix x))
rw Dim (Matrix x) (Point (Matrix x))
cl forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x i j. Additive x => Entries i j x -> Entries i j x
etsElimZeros forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i j x. PSequence (i, j) x -> Entries i j x
Entries forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x (n :: N').
Distributive x =>
N -> FinList n (Matrix x) -> [(Matrix x, (N, N))]
u N
0 FinList n (Matrix x)
cs where
      rw :: Dim (Matrix x) (Point (Matrix x))
rw = forall p x. (Entity p, p ~ Point x) => [p] -> Dim x p
productDim forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall q. Oriented q => q -> Point q
end FinList n (Matrix x)
cs
      cl :: Dim (Matrix x) (Point (Matrix x))
cl = forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim Point (Matrix x)
t
      
      u :: Distributive x => N -> FinList n (Matrix x) -> [(Matrix x,(N,N))]
      u :: forall x (n :: N').
Distributive x =>
N -> FinList n (Matrix x) -> [(Matrix x, (N, N))]
u N
_ FinList n (Matrix x)
Nil     = []
      u N
i (Matrix x
c:|FinList n (Matrix x)
cs) = (Matrix x
c,(N
i,N
0)) forall a. a -> [a] -> [a]
: forall x (n :: N').
Distributive x =>
N -> FinList n (Matrix x) -> [(Matrix x, (N, N))]
u (forall a. Enum a => a -> a
succ N
i) FinList n (Matrix x)
cs 
  
--------------------------------------------------------------------------------
-- mtxSums -

-- | sums for matrices.
mtxSums :: Distributive x => Sums n (Matrix x)
mtxSums :: forall x (n :: N'). Distributive x => Sums n (Matrix x)
mtxSums = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Sums n) (Products n) a
sumLimitsDuality forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
IsoOrt s h =>
h a b -> Limits s p t n m a -> Limits s p t n m b
lmsMap forall x.
Distributive x =>
IsoOpMap Matrix Dst (Matrix (Op x)) (Op (Matrix x))
isoToOp forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x (n :: N'). Distributive x => Products n (Matrix x)
mtxProducts where
  isoToOp :: Distributive x => IsoOpMap Matrix Dst (Matrix (Op x)) (Op (Matrix x)) 
  isoToOp :: forall x.
Distributive x =>
IsoOpMap Matrix Dst (Matrix (Op x)) (Op (Matrix x))
isoToOp = forall (c :: * -> * -> *) x y. Cayleyan2 c => c x y -> c y x
invert2 forall x.
Distributive x =>
IsoOpMap Matrix Dst (Op (Matrix x)) (Matrix (Op x))
isoCoMatrixDst