{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Entity.Matrix.Transformation
-- Description : elementary matrix transformations
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- elementary matrix transformations, i.e. operations of 'GLT' on 'Matrix'.
module OAlg.Entity.Matrix.Transformation
  ( -- * Row Trafo
    RowTrafo(..), crTrafoRows

    -- * Col Trafo
  , ColTrafo(..), crTrafoCols

    -- * Diagonal Form
  , DiagonalForm(..), dgfMatrix
  , DiagonalFormStrictPositive(..)
  )

  where

import Control.Monad

import Data.List (length,map)

import OAlg.Prelude

import OAlg.Data.Canonical

import OAlg.Structure.Exception
import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Distributive
import OAlg.Structure.Number
import OAlg.Structure.Ring
import OAlg.Structure.Exponential
import OAlg.Structure.Operational

import OAlg.Entity.Product

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

--------------------------------------------------------------------------------
-- crShearRows -

-- | shears tow rows of a /matrix/.
--
--   __Pre__ @k '<' l@.
crShearRows :: (Distributive x, Ord i, Ord j)
  => i -> i -> GL2 x
  -> Col i (Row j x) -> Col i (Row j x)
crShearRows :: forall x i j.
(Distributive x, Ord i, Ord j) =>
i -> i -> GL2 x -> Col i (Row j x) -> Col i (Row j x)
crShearRows i
k i
l (GL2 x
s x
t x
u x
v) = forall i s x.
Ord i =>
(s -> Maybe x -> Maybe x)
-> (Maybe x -> Maybe x -> Maybe x)
-> i
-> i
-> s
-> s
-> s
-> s
-> Col i x
-> Col i x
colShear forall {a} {j}.
Distributive a =>
a -> Maybe (Row j a) -> Maybe (Row j a)
(*>) forall {a} {j}.
(Additive a, Ord j) =>
Maybe (Row j a) -> Maybe (Row j a) -> Maybe (Row j a)
(<+>) i
k i
l x
s x
t x
u x
v where

  a
_ *> :: a -> Maybe (Row j a) -> Maybe (Row j a)
*> Maybe (Row j a)
Nothing   = forall a. Maybe a
Nothing
  a
a *> (Just Row j a
rw) = forall a. (a -> Bool) -> a -> Maybe a
just (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall j x. Row j x -> Bool
rowIsEmpty) (a
a forall a j. Distributive a => a -> Row j a -> Row j a
`rowMltl` Row j a
rw)

  Maybe (Row j a)
a <+> :: Maybe (Row j a) -> Maybe (Row j a) -> Maybe (Row j a)
<+> Maybe (Row j a)
Nothing     = Maybe (Row j a)
a
  Maybe (Row j a)
Nothing <+> Maybe (Row j a)
b     = Maybe (Row j a)
b
  Just Row j a
a <+> Just Row j a
b = forall a. (a -> Bool) -> a -> Maybe a
just (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall j x. Row j x -> Bool
rowIsEmpty) (Row j a
a forall a j. (Additive a, Ord j) => Row j a -> Row j a -> Row j a
`rowAdd` Row j a
b)

--------------------------------------------------------------------------------
-- crShearCols -

-- | shears the tow columns of a /matrix/.
--
--   __Pre__ @k '<' l@.
crShearCols :: (Distributive x, Ord j)
  => j -> j -> GL2 x
  -> Col i (Row j x) -> Col i (Row j x)
crShearCols :: forall x j i.
(Distributive x, Ord j) =>
j -> j -> GL2 x -> Col i (Row j x) -> Col i (Row j x)
crShearCols j
k j
l (GL2 x
s x
t x
u x
v) Col i (Row j x)
rws
  = forall x i. (x -> Bool) -> Col i x -> Col i x
colFilter (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall j x. Row j x -> Bool
rowIsEmpty) 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 j x s.
Ord j =>
(Maybe x -> s -> Maybe x)
-> (Maybe x -> Maybe x -> Maybe x)
-> j
-> j
-> s
-> s
-> s
-> s
-> Row j x
-> Row j x
rowShear forall {a}.
(Additive a, Multiplicative a) =>
Maybe a -> a -> Maybe a
(<*$) forall {a}. Additive a => Maybe a -> Maybe a -> Maybe a
(<+>) j
k j
l x
s x
t x
u x
v) Col i (Row j x)
rws where
  
  Maybe a
Nothing <*$ :: Maybe a -> a -> Maybe a
<*$ a
_  = forall a. Maybe a
Nothing
  (Just a
x) <*$ a
r = forall a. (a -> Bool) -> a -> Maybe a
just (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall a. Additive a => a -> Bool
isZero) (a
xforall c. Multiplicative c => c -> c -> c
*a
r) 

  Maybe a
a <+> :: Maybe a -> Maybe a -> Maybe a
<+> Maybe a
Nothing     = Maybe a
a
  Maybe a
Nothing <+> Maybe a
b     = Maybe a
b
  Just a
a <+> Just a
b = forall a. (a -> Bool) -> a -> Maybe a
just (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall a. Additive a => a -> Bool
isZero) (a
aforall a. Additive a => a -> a -> a
+a
b) 

--------------------------------------------------------------------------------
-- crScaleRow -

crScaleRow :: (Distributive x, Ord i)
  => i -> Inv x -> Col i (Row j x) -> Col i (Row j x)
crScaleRow :: forall x i j.
(Distributive x, Ord i) =>
i -> Inv x -> Col i (Row j x) -> Col i (Row j x)
crScaleRow i
i Inv x
a Col i (Row j x)
cl = forall i s x.
Ord i =>
(s -> x -> Maybe x) -> i -> s -> Col i x -> Col i x
colScale forall {a} {j}. Distributive a => a -> Row j a -> Maybe (Row j a)
(*>) i
i (forall a b. Embeddable a b => a -> b
inj Inv x
a) Col i (Row j x)
cl where
  a
a *> :: a -> Row j a -> Maybe (Row j a)
*> Row j a
rw = forall a. (a -> Bool) -> a -> Maybe a
just (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall j x. Row j x -> Bool
rowIsEmpty) (a
a forall a j. Distributive a => a -> Row j a -> Row j a
`rowMltl` Row j a
rw)

--------------------------------------------------------------------------------
-- crScaleCol -

crScaleCol :: (Distributive x, Ord j)
  => j -> Inv x -> Col i (Row j x) -> Col i (Row j x)
crScaleCol :: forall x j i.
(Distributive x, Ord j) =>
j -> Inv x -> Col i (Row j x) -> Col i (Row j x)
crScaleCol j
j Inv x
a Col i (Row j x)
rws
  = forall x i. (x -> Bool) -> Col i x -> Col i x
colFilter (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall j x. Row j x -> Bool
rowIsEmpty) 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 j x s.
Ord j =>
(x -> s -> Maybe x) -> j -> s -> Row j x -> Row j x
rowScale forall {a}. (Additive a, Multiplicative a) => a -> a -> Maybe a
(<*$) j
j (forall a b. Embeddable a b => a -> b
inj Inv x
a)) Col i (Row j x)
rws where
  a
x <*$ :: a -> a -> Maybe a
<*$ a
s = forall a. (a -> Bool) -> a -> Maybe a
just (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall a. Additive a => a -> Bool
isZero) (a
xforall c. Multiplicative c => c -> c -> c
*a
s)

--------------------------------------------------------------------------------
-- rcScaleCol -

rcScaleCol :: (Distributive x, Ord j)
  => j -> Inv x -> Row j (Col i x) -> Row j (Col i x)
rcScaleCol :: forall x j i.
(Distributive x, Ord j) =>
j -> Inv x -> Row j (Col i x) -> Row j (Col i x)
rcScaleCol j
j Inv x
a Row j (Col i x)
cls = forall j x s.
Ord j =>
(x -> s -> Maybe x) -> j -> s -> Row j x -> Row j x
rowScale forall {a} {i}. Distributive a => Col i a -> a -> Maybe (Col i a)
(<*$) j
j (forall a b. Embeddable a b => a -> b
inj Inv x
a) Row j (Col i x)
cls where
  Col i a
cl <*$ :: Col i a -> a -> Maybe (Col i a)
<*$ a
a = forall a. (a -> Bool) -> a -> Maybe a
just (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall i x. Col i x -> Bool
colIsEmpty) (Col i a
cl forall a i. Distributive a => Col i a -> a -> Col i a
`colMltr` a
a)

--------------------------------------------------------------------------------
-- rcShearCols -

rcShearCols :: (Distributive x, Ord i, Ord j)
  => j -> j -> GL2 x
  -> Row j (Col i x) -> Row j (Col i x)
rcShearCols :: forall x i j.
(Distributive x, Ord i, Ord j) =>
j -> j -> GL2 x -> Row j (Col i x) -> Row j (Col i x)
rcShearCols j
k j
l (GL2 x
s x
t x
u x
v) = forall j x s.
Ord j =>
(Maybe x -> s -> Maybe x)
-> (Maybe x -> Maybe x -> Maybe x)
-> j
-> j
-> s
-> s
-> s
-> s
-> Row j x
-> Row j x
rowShear forall {a} {i}.
Distributive a =>
Maybe (Col i a) -> a -> Maybe (Col i a)
(<*$) forall {a} {i}.
(Additive a, Ord i) =>
Maybe (Col i a) -> Maybe (Col i a) -> Maybe (Col i a)
(<+>) j
k j
l x
s x
t x
u x
v where
  Maybe (Col i a)
Nothing <*$ :: Maybe (Col i a) -> a -> Maybe (Col i a)
<*$ a
_   = forall a. Maybe a
Nothing
  (Just Col i a
cl) <*$ a
a = forall a. (a -> Bool) -> a -> Maybe a
just (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall i x. Col i x -> Bool
colIsEmpty) (Col i a
cl forall a i. Distributive a => Col i a -> a -> Col i a
`colMltr` a
a)
  
  Maybe (Col i a)
a <+> :: Maybe (Col i a) -> Maybe (Col i a) -> Maybe (Col i a)
<+> Maybe (Col i a)
Nothing     = Maybe (Col i a)
a
  Maybe (Col i a)
Nothing <+> Maybe (Col i a)
b     = Maybe (Col i a)
b
  Just Col i a
a <+> Just Col i a
b = forall a. (a -> Bool) -> a -> Maybe a
just (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall i x. Col i x -> Bool
colIsEmpty) (Col i a
a forall a i. (Additive a, Ord i) => Col i a -> Col i a -> Col i a
`colAdd` Col i a
b)

--------------------------------------------------------------------------------
-- crTrafoRows -

-- | applying a transformation as a row transformation on a column of rows.
crTrafoRows :: Transformation x -> Col N (Row N x) -> Col N (Row N x)
crTrafoRows :: forall x. Transformation x -> Col N (Row N x) -> Col N (Row N x)
crTrafoRows (Permute Dim x (Point x)
_ Dim x (Point x)
_ Permutation N
p) Col N (Row N x)
rws = Col N (Row N x)
rws forall f x. Opr f x => x -> f -> x
<* Permutation N
p
crTrafoRows (Scale Dim x (Point x)
_ N
k Inv x
s) Col N (Row N x)
rws   = forall x i j.
(Distributive x, Ord i) =>
i -> Inv x -> Col i (Row j x) -> Col i (Row j x)
crScaleRow N
k Inv x
s Col N (Row N x)
rws
crTrafoRows (Shear Dim x (Point x)
_ N
k N
l GL2 x
g) Col N (Row N x)
rws = forall x i j.
(Distributive x, Ord i, Ord j) =>
i -> i -> GL2 x -> Col i (Row j x) -> Col i (Row j x)
crShearRows N
k N
l GL2 x
g Col N (Row N x)
rws

--------------------------------------------------------------------------------
-- crTrafoCols -

-- | applying a transformation as a column transformation on a column of rows.
crTrafoCols :: Col N (Row N x) -> Transformation x -> Col N (Row N x)
crTrafoCols :: forall x. Col N (Row N x) -> Transformation x -> Col N (Row N x)
crTrafoCols Col N (Row N x)
rws (Permute Dim x (Point x)
_ Dim x (Point x)
_ Permutation N
p) = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall f x. Opr f x => x -> f -> x
<*Permutation N
p') Col N (Row N x)
rws where p' :: Permutation N
p' = forall c. Invertible c => c -> c
invert Permutation N
p
crTrafoCols Col N (Row N x)
rws (Scale Dim x (Point x)
_ N
k Inv x
s)   = forall x j i.
(Distributive x, Ord j) =>
j -> Inv x -> Col i (Row j x) -> Col i (Row j x)
crScaleCol N
k Inv x
s Col N (Row N x)
rws
crTrafoCols Col N (Row N x)
rws (Shear Dim x (Point x)
_ N
k N
l GL2 x
g) = forall x j i.
(Distributive x, Ord j) =>
j -> j -> GL2 x -> Col i (Row j x) -> Col i (Row j x)
crShearCols N
k N
l GL2 x
g Col N (Row N x)
rws

--------------------------------------------------------------------------------
-- rcTrafoCols -

-- | applying a transformation as a column transformation on a row of columns.
rcTrafoCols :: Row N (Col N x) -> Transformation x -> Row N (Col N x)
rcTrafoCols :: forall x. Row N (Col N x) -> Transformation x -> Row N (Col N x)
rcTrafoCols Row N (Col N x)
cls (Permute Dim x (Point x)
_ Dim x (Point x)
_ Permutation N
p) = Row N (Col N x)
cls forall f x. Opr f x => x -> f -> x
<* Permutation N
p' where p' :: Permutation N
p' = forall c. Invertible c => c -> c
invert Permutation N
p
rcTrafoCols Row N (Col N x)
cls (Scale Dim x (Point x)
_ N
k Inv x
s)   = forall x j i.
(Distributive x, Ord j) =>
j -> Inv x -> Row j (Col i x) -> Row j (Col i x)
rcScaleCol N
k Inv x
s Row N (Col N x)
cls
rcTrafoCols Row N (Col N x)
cls (Shear Dim x (Point x)
_ N
k N
l GL2 x
g) = forall x i j.
(Distributive x, Ord i, Ord j) =>
j -> j -> GL2 x -> Row j (Col i x) -> Row j (Col i x)
rcShearCols N
k N
l GL2 x
g Row N (Col N x)
cls

--------------------------------------------------------------------------------
-- ColTrafo -

-- | 'GLT' as a column transformation.
newtype ColTrafo x = ColTrafo (GLT x)  
  deriving ( ColTrafo x -> ColTrafo x -> Bool
forall x. Oriented x => ColTrafo x -> ColTrafo x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ColTrafo x -> ColTrafo x -> Bool
$c/= :: forall x. Oriented x => ColTrafo x -> ColTrafo x -> Bool
== :: ColTrafo x -> ColTrafo x -> Bool
$c== :: forall x. Oriented x => ColTrafo x -> ColTrafo x -> Bool
Eq,Int -> ColTrafo x -> ShowS
forall x. Oriented x => Int -> ColTrafo x -> ShowS
forall x. Oriented x => [ColTrafo x] -> ShowS
forall x. Oriented x => ColTrafo x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ColTrafo x] -> ShowS
$cshowList :: forall x. Oriented x => [ColTrafo x] -> ShowS
show :: ColTrafo x -> String
$cshow :: forall x. Oriented x => ColTrafo x -> String
showsPrec :: Int -> ColTrafo x -> ShowS
$cshowsPrec :: forall x. Oriented x => Int -> ColTrafo x -> ShowS
Show,ColTrafo x -> Statement
forall x. Oriented x => ColTrafo x -> Statement
forall a. (a -> Statement) -> Validable a
valid :: ColTrafo x -> Statement
$cvalid :: forall x. Oriented x => ColTrafo x -> Statement
Validable,forall a. Show a -> Eq a -> Validable a -> Typeable a -> Entity a
forall x. Oriented x => Eq (ColTrafo x)
forall x. Oriented x => Show (ColTrafo x)
forall {x}. Oriented x => Typeable (ColTrafo x)
forall x. Oriented x => Validable (ColTrafo x)
Entity
           , Point (ColTrafo x) -> ColTrafo x
ColTrafo x -> N -> ColTrafo x
ColTrafo x -> ColTrafo x -> ColTrafo x
forall {x}. Oriented x => Oriented (ColTrafo x)
forall x. Oriented x => Point (ColTrafo x) -> ColTrafo x
forall x. Oriented x => ColTrafo x -> N -> ColTrafo x
forall x. Oriented x => ColTrafo x -> ColTrafo x -> ColTrafo x
forall c.
Oriented c
-> (Point c -> c)
-> (c -> c -> c)
-> (c -> N -> c)
-> Multiplicative c
npower :: ColTrafo x -> N -> ColTrafo x
$cnpower :: forall x. Oriented x => ColTrafo x -> N -> ColTrafo x
* :: ColTrafo x -> ColTrafo x -> ColTrafo x
$c* :: forall x. Oriented x => ColTrafo x -> ColTrafo x -> ColTrafo x
one :: Point (ColTrafo x) -> ColTrafo x
$cone :: forall x. Oriented x => Point (ColTrafo x) -> ColTrafo x
Multiplicative, ColTrafo x -> Bool
ColTrafo x -> Solver (ColTrafo x)
ColTrafo x -> ColTrafo x
ColTrafo x -> Z -> ColTrafo x
forall x. Oriented x => Multiplicative (ColTrafo x)
forall x. Oriented x => ColTrafo x -> Bool
forall x. Oriented x => ColTrafo x -> Solver (ColTrafo x)
forall x. Oriented x => ColTrafo x -> ColTrafo x
forall x. Oriented x => ColTrafo x -> Z -> ColTrafo x
forall c.
Multiplicative c
-> (c -> Solver c)
-> (c -> c)
-> (c -> Bool)
-> (c -> Z -> c)
-> Invertible c
zpower :: ColTrafo x -> Z -> ColTrafo x
$czpower :: forall x. Oriented x => ColTrafo x -> Z -> ColTrafo x
isInvertible :: ColTrafo x -> Bool
$cisInvertible :: forall x. Oriented x => ColTrafo x -> Bool
invert :: ColTrafo x -> ColTrafo x
$cinvert :: forall x. Oriented x => ColTrafo x -> ColTrafo x
tryToInvert :: ColTrafo x -> Solver (ColTrafo x)
$ctryToInvert :: forall x. Oriented x => ColTrafo x -> Solver (ColTrafo x)
Invertible, forall x. Oriented x => Invertible (ColTrafo x)
forall c. Invertible c -> Cayleyan c
Cayleyan
           )

instance Oriented x => Oriented (ColTrafo x) where
  type Point (ColTrafo x) = Dim x (Point x)
  orientation :: ColTrafo x -> Orientation (Point (ColTrafo x))
orientation (ColTrafo GLT x
t) = forall q. Oriented q => q -> Orientation (Point q)
orientation GLT x
t

instance Oriented x => Exponential (ColTrafo x) where
  type Exponent (ColTrafo x) = Z
  ColTrafo GLT x
t ^ :: ColTrafo x -> Exponent (ColTrafo x) -> ColTrafo x
^ Exponent (ColTrafo x)
z = forall x. GLT x -> ColTrafo x
ColTrafo (GLT x
tforall f. Exponential f => f -> Exponent f -> f
^Exponent (ColTrafo x)
z)

--------------------------------------------------------------------------------
-- ColTrafo - OrientedOpr -

instance Oriented x => Opr (ColTrafo x) (Matrix x) where
  Matrix Dim x (Point x)
r Dim x (Point x)
c Entries N N x
xs <* :: Matrix x -> ColTrafo x -> Matrix x
<* (ColTrafo GLT x
t)
    | Point (GLT x)
d forall a. Eq a => a -> a -> Bool
== Dim x (Point x)
c    = forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim x (Point x)
r (forall q. Oriented q => q -> Point q
start GLT x
t) (forall i j x. (Ord i, Ord j) => Row j (Col i x) -> Entries i j x
rcets (forall i j x. (Ord i, Ord j) => Entries i j x -> Row j (Col i x)
etsrc Entries N N x
xs Row N (Col N x)
-> ProductForm N (Transformation x) -> Row N (Col N x)
<| forall a b. Embeddable a b => a -> b
inj GLT x
t))
                  -- for a justification for the expression inj t see rdcGLTForm
                  -- respectively the properties of GLT 
    | Bool
otherwise = forall a e. Exception e => e -> a
throw ArithmeticException
NotApplicable
    where d :: Point (GLT x)
d    = forall q. Oriented q => q -> Point q
end GLT x
t 
          <| :: Row N (Col N x)
-> ProductForm N (Transformation x) -> Row N (Col N x)
(<|) = forall x t. N -> (x -> t -> x) -> x -> ProductForm N t -> x
prfopr' N
n forall x. Row N (Col N x) -> Transformation x -> Row N (Col N x)
rcTrafoCols
          n :: N
n    = N
10 forall a. Ord a => a -> a -> a
`max` (forall x. LengthN x => x -> N
lengthN Point (GLT x)
d forall a. Integral a => a -> a -> a
`div` N
2)

instance Distributive x => OrientedOpr (ColTrafo x) (Matrix x)

--------------------------------------------------------------------------------
-- RowTrafo -

-- | 'GLT' as row transformations.
newtype RowTrafo a = RowTrafo (GLT a)
  deriving ( RowTrafo a -> RowTrafo a -> Bool
forall a. Oriented a => RowTrafo a -> RowTrafo a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RowTrafo a -> RowTrafo a -> Bool
$c/= :: forall a. Oriented a => RowTrafo a -> RowTrafo a -> Bool
== :: RowTrafo a -> RowTrafo a -> Bool
$c== :: forall a. Oriented a => RowTrafo a -> RowTrafo a -> Bool
Eq,Int -> RowTrafo a -> ShowS
forall a. Oriented a => Int -> RowTrafo a -> ShowS
forall a. Oriented a => [RowTrafo a] -> ShowS
forall a. Oriented a => RowTrafo a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RowTrafo a] -> ShowS
$cshowList :: forall a. Oriented a => [RowTrafo a] -> ShowS
show :: RowTrafo a -> String
$cshow :: forall a. Oriented a => RowTrafo a -> String
showsPrec :: Int -> RowTrafo a -> ShowS
$cshowsPrec :: forall a. Oriented a => Int -> RowTrafo a -> ShowS
Show,RowTrafo a -> Statement
forall a. Oriented a => RowTrafo a -> Statement
forall a. (a -> Statement) -> Validable a
valid :: RowTrafo a -> Statement
$cvalid :: forall a. Oriented a => RowTrafo a -> Statement
Validable,forall a. Show a -> Eq a -> Validable a -> Typeable a -> Entity a
forall a. Oriented a => Eq (RowTrafo a)
forall a. Oriented a => Show (RowTrafo a)
forall {a}. Oriented a => Typeable (RowTrafo a)
forall a. Oriented a => Validable (RowTrafo a)
Entity
           , Point (RowTrafo a) -> RowTrafo a
RowTrafo a -> N -> RowTrafo a
RowTrafo a -> RowTrafo a -> RowTrafo a
forall {a}. Oriented a => Oriented (RowTrafo a)
forall a. Oriented a => Point (RowTrafo a) -> RowTrafo a
forall a. Oriented a => RowTrafo a -> N -> RowTrafo a
forall a. Oriented a => RowTrafo a -> RowTrafo a -> RowTrafo a
forall c.
Oriented c
-> (Point c -> c)
-> (c -> c -> c)
-> (c -> N -> c)
-> Multiplicative c
npower :: RowTrafo a -> N -> RowTrafo a
$cnpower :: forall a. Oriented a => RowTrafo a -> N -> RowTrafo a
* :: RowTrafo a -> RowTrafo a -> RowTrafo a
$c* :: forall a. Oriented a => RowTrafo a -> RowTrafo a -> RowTrafo a
one :: Point (RowTrafo a) -> RowTrafo a
$cone :: forall a. Oriented a => Point (RowTrafo a) -> RowTrafo a
Multiplicative, RowTrafo a -> Bool
RowTrafo a -> Solver (RowTrafo a)
RowTrafo a -> RowTrafo a
RowTrafo a -> Z -> RowTrafo a
forall a. Oriented a => Multiplicative (RowTrafo a)
forall a. Oriented a => RowTrafo a -> Bool
forall a. Oriented a => RowTrafo a -> Solver (RowTrafo a)
forall a. Oriented a => RowTrafo a -> RowTrafo a
forall a. Oriented a => RowTrafo a -> Z -> RowTrafo a
forall c.
Multiplicative c
-> (c -> Solver c)
-> (c -> c)
-> (c -> Bool)
-> (c -> Z -> c)
-> Invertible c
zpower :: RowTrafo a -> Z -> RowTrafo a
$czpower :: forall a. Oriented a => RowTrafo a -> Z -> RowTrafo a
isInvertible :: RowTrafo a -> Bool
$cisInvertible :: forall a. Oriented a => RowTrafo a -> Bool
invert :: RowTrafo a -> RowTrafo a
$cinvert :: forall a. Oriented a => RowTrafo a -> RowTrafo a
tryToInvert :: RowTrafo a -> Solver (RowTrafo a)
$ctryToInvert :: forall a. Oriented a => RowTrafo a -> Solver (RowTrafo a)
Invertible, forall a. Oriented a => Invertible (RowTrafo a)
forall c. Invertible c -> Cayleyan c
Cayleyan
           )

instance Oriented a => Oriented (RowTrafo a) where
  type Point (RowTrafo a) = Dim a (Point a)
  orientation :: RowTrafo a -> Orientation (Point (RowTrafo a))
orientation (RowTrafo GLT a
t) = forall q. Oriented q => q -> Orientation (Point q)
orientation GLT a
t

instance Oriented a => Exponential (RowTrafo a) where
  type Exponent (RowTrafo a) = Z
  RowTrafo GLT a
t ^ :: RowTrafo a -> Exponent (RowTrafo a) -> RowTrafo a
^ Exponent (RowTrafo a)
z = forall a. GLT a -> RowTrafo a
RowTrafo (GLT a
tforall f. Exponential f => f -> Exponent f -> f
^Exponent (RowTrafo a)
z)

--------------------------------------------------------------------------------
-- RowTrafo - OrientedOpl -

instance Oriented x => Opl (RowTrafo x) (Matrix x) where
  RowTrafo GLT x
t *> :: RowTrafo x -> Matrix x -> Matrix x
*> Matrix Dim x (Point x)
r Dim x (Point x)
c Entries N N x
xs
    | Point (GLT x)
d forall a. Eq a => a -> a -> Bool
== Dim x (Point x)
r    = forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix (forall q. Oriented q => q -> Point q
end GLT x
t) Dim x (Point x)
c forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i j x. Col i (Row j x) -> Entries i j x
crets (forall a b. Embeddable a b => a -> b
inj GLT x
t ProductForm N (Transformation x)
-> Col N (Row N x) -> Col N (Row N x)
|> forall i j x. Eq i => Entries i j x -> Col i (Row j x)
etscr Entries N N x
xs)
                  -- for a justification for the expression inj t see rdcGLTForm
                  -- respectively the properties of GLT 
    | Bool
otherwise = forall a e. Exception e => e -> a
throw ArithmeticException
NotApplicable
    where d :: Point (GLT x)
d = forall q. Oriented q => q -> Point q
start GLT x
t
          |> :: ProductForm N (Transformation x)
-> Col N (Row N x) -> Col N (Row N x)
(|>) = forall t x. N -> (t -> x -> x) -> ProductForm N t -> x -> x
prfopl' N
n forall x. Transformation x -> Col N (Row N x) -> Col N (Row N x)
crTrafoRows
          n :: N
n    = N
10 forall a. Ord a => a -> a -> a
`max` (forall x. LengthN x => x -> N
lengthN Point (GLT x)
d forall a. Integral a => a -> a -> a
`div` N
2)

instance Distributive x => OrientedOpl (RowTrafo x) (Matrix x)

--------------------------------------------------------------------------------
-- DiagonalForm -

-- | the result of transforming a matrix into a diagonal form.
--
-- __Property__ Let @'DiagonalForm' ds rt ct@ be in @'DiagonalForm' __k__@, then holds:
--
-- (1) @n '<=' 'lengthN' ('start' rt)@ and @n '<=' 'lengthN' ('end' ct)@ where
-- @n = 'lengthN' ds@.
--
-- (2) For all @d@ in @ds@ holds: @'not' ('isZero' d)@.
data DiagonalForm k = DiagonalForm [k] (RowTrafo k) (ColTrafo k) deriving (DiagonalForm k -> DiagonalForm k -> Bool
forall k. Oriented k => DiagonalForm k -> DiagonalForm k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiagonalForm k -> DiagonalForm k -> Bool
$c/= :: forall k. Oriented k => DiagonalForm k -> DiagonalForm k -> Bool
== :: DiagonalForm k -> DiagonalForm k -> Bool
$c== :: forall k. Oriented k => DiagonalForm k -> DiagonalForm k -> Bool
Eq,Int -> DiagonalForm k -> ShowS
forall k. Oriented k => Int -> DiagonalForm k -> ShowS
forall k. Oriented k => [DiagonalForm k] -> ShowS
forall k. Oriented k => DiagonalForm k -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiagonalForm k] -> ShowS
$cshowList :: forall k. Oriented k => [DiagonalForm k] -> ShowS
show :: DiagonalForm k -> String
$cshow :: forall k. Oriented k => DiagonalForm k -> String
showsPrec :: Int -> DiagonalForm k -> ShowS
$cshowsPrec :: forall k. Oriented k => Int -> DiagonalForm k -> ShowS
Show)

--------------------------------------------------------------------------------
-- DiagonalForm - Entity -

instance Distributive k => Validable (DiagonalForm k) where
  valid :: DiagonalForm k -> Statement
valid (DiagonalForm [k]
ds RowTrafo k
rt ColTrafo k
ct) = String -> Label
Label String
"DiagonalForm" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid ([k]
ds,RowTrafo k
rt,ColTrafo k
ct)
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>:
            (forall x. LengthN x => x -> N
lengthN [k]
ds forall a. Ord a => a -> a -> Bool
<= forall a. Ord a => a -> a -> a
min (forall x. LengthN x => x -> N
lengthN (forall q. Oriented q => q -> Point q
start RowTrafo k
rt)) (forall x. LengthN x => x -> N
lengthN (forall q. Oriented q => q -> Point q
end ColTrafo k
ct)))
              Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[ String
"lengthN ds"String -> String -> Parameter
:=forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [k]
ds)
                       , String
"lengthN (start rt)"String -> String -> Parameter
:= forall a. Show a => a -> String
show (forall x. LengthN x => x -> N
lengthN (forall q. Oriented q => q -> Point q
start RowTrafo k
rt))
                       , String
"lengthN (end ct)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (forall x. LengthN x => x -> N
lengthN (forall q. Oriented q => q -> Point q
end ColTrafo k
ct))
                       ]
        , String -> Label
Label String
"2"
            Label -> Statement -> Statement
:<=>: (forall b. Boolean b => [b] -> b
and forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall b. Boolean b => b -> b
notforall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.forall a. Additive a => a -> Bool
isZero) [k]
ds) Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"ds"String -> String -> Parameter
:=forall a. Show a => a -> String
show [k]
ds]
        ]

instance Distributive k => Entity (DiagonalForm k)

--------------------------------------------------------------------------------
-- dgfMatrix -

-- | the resulting matrix by applying on the diagonal matrix the inverse of the
-- given transformations.
dgfMatrix :: Distributive k => DiagonalForm k -> Matrix k
dgfMatrix :: forall k. Distributive k => DiagonalForm k -> Matrix k
dgfMatrix (DiagonalForm [k]
ds RowTrafo k
rt ColTrafo k
ct) = (RowTrafo k
rt'forall f x. Opl f x => f -> x -> x
*>Matrix k
dm)forall f x. Opr f x => x -> f -> x
<*ColTrafo k
ct' where
  rt' :: RowTrafo k
rt' = forall c. Invertible c => c -> c
invert RowTrafo k
rt
  ct' :: ColTrafo k
ct' = forall c. Invertible c => c -> c
invert ColTrafo k
ct
  dm :: Matrix k
dm = forall x. Additive x => Dim' x -> Dim' x -> [x] -> Matrix x
diagonal (forall q. Oriented q => q -> Point q
start RowTrafo k
rt') (forall q. Oriented q => q -> Point q
end ColTrafo k
ct') [k]
ds


--------------------------------------------------------------------------------
-- DiagonalFormStrictPositive -

-- | predicate for diagonal forms with strict positive entries.
--
-- __Property__ Let @'DiagonalFormStrictPositive' ('DiagonalForm' ds _ _)@ be in
-- @'DiagonalForm' __k__@, then holds: @0 '<' d@ for all @d@ in @ds@. 
newtype DiagonalFormStrictPositive k
  = DiagonalFormStrictPositive (DiagonalForm k)
 deriving (Int -> DiagonalFormStrictPositive k -> ShowS
forall k.
Oriented k =>
Int -> DiagonalFormStrictPositive k -> ShowS
forall k. Oriented k => [DiagonalFormStrictPositive k] -> ShowS
forall k. Oriented k => DiagonalFormStrictPositive k -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiagonalFormStrictPositive k] -> ShowS
$cshowList :: forall k. Oriented k => [DiagonalFormStrictPositive k] -> ShowS
show :: DiagonalFormStrictPositive k -> String
$cshow :: forall k. Oriented k => DiagonalFormStrictPositive k -> String
showsPrec :: Int -> DiagonalFormStrictPositive k -> ShowS
$cshowsPrec :: forall k.
Oriented k =>
Int -> DiagonalFormStrictPositive k -> ShowS
Show,DiagonalFormStrictPositive k
-> DiagonalFormStrictPositive k -> Bool
forall k.
Oriented k =>
DiagonalFormStrictPositive k
-> DiagonalFormStrictPositive k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiagonalFormStrictPositive k
-> DiagonalFormStrictPositive k -> Bool
$c/= :: forall k.
Oriented k =>
DiagonalFormStrictPositive k
-> DiagonalFormStrictPositive k -> Bool
== :: DiagonalFormStrictPositive k
-> DiagonalFormStrictPositive k -> Bool
$c== :: forall k.
Oriented k =>
DiagonalFormStrictPositive k
-> DiagonalFormStrictPositive k -> Bool
Eq)

instance Number k => Validable (DiagonalFormStrictPositive k) where
  valid :: DiagonalFormStrictPositive k -> Statement
valid (DiagonalFormStrictPositive f :: DiagonalForm k
f@(DiagonalForm [k]
ds RowTrafo k
_ ColTrafo k
_))
    = String -> Label
Label String
"DiagonalFormStrictPositive" Label -> Statement -> Statement
:<=>:
      [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid DiagonalForm k
f
          , forall {a} {t}.
(Ord a, Distributive a, Total a, Enum t, Show t) =>
t -> [a] -> Statement
vld (N
0::N) [k]
ds
          ] where
    vld :: t -> [a] -> Statement
vld t
_ []     = Statement
SValid
    vld t
i (a
d:[a]
ds) = [Statement] -> Statement
And [ (forall r. Semiring r => r
rZero forall a. Ord a => a -> a -> Bool
< a
d)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(d,i)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (a
d,t
i)]
                       , t -> [a] -> Statement
vld (forall a. Enum a => a -> a
succ t
i) [a]
ds
                       ]
                   
instance Number k => Entity (DiagonalFormStrictPositive k)