{-# 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) = (x -> Maybe (Row j x) -> Maybe (Row j x))
-> (Maybe (Row j x) -> Maybe (Row j x) -> Maybe (Row j x))
-> i
-> i
-> x
-> x
-> x
-> x
-> Col i (Row j x)
-> Col i (Row j x)
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 x -> Maybe (Row j x) -> Maybe (Row j x)
forall {a} {j}.
Distributive a =>
a -> Maybe (Row j a) -> Maybe (Row j a)
(*>) Maybe (Row j x) -> Maybe (Row j x) -> Maybe (Row j x)
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   = Maybe (Row j a)
forall a. Maybe a
Nothing
  a
a *> (Just Row j a
rw) = (Row j a -> Bool) -> Row j a -> Maybe (Row j a)
forall a. (a -> Bool) -> a -> Maybe a
just (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (Row j a -> Bool) -> Row j a -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.Row j a -> Bool
forall j x. Row j x -> Bool
rowIsEmpty) (a
a a -> Row j a -> Row j 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 = (Row j a -> Bool) -> Row j a -> Maybe (Row j a)
forall a. (a -> Bool) -> a -> Maybe a
just (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (Row j a -> Bool) -> Row j a -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.Row j a -> Bool
forall j x. Row j x -> Bool
rowIsEmpty) (Row j a
a Row j a -> Row j a -> Row j 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
  = (Row j x -> Bool) -> Col i (Row j x) -> Col i (Row j x)
forall x i. (x -> Bool) -> Col i x -> Col i x
colFilter (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (Row j x -> Bool) -> Row j x -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.Row j x -> Bool
forall j x. Row j x -> Bool
rowIsEmpty) (Col i (Row j x) -> Col i (Row j x))
-> Col i (Row j x) -> Col i (Row j x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Row j x -> Row j x) -> Col i (Row j x) -> Col i (Row j x)
forall a b. (a -> b) -> Col i a -> Col i b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Maybe x -> x -> Maybe x)
-> (Maybe x -> Maybe x -> Maybe x)
-> j
-> j
-> x
-> x
-> x
-> x
-> Row j x
-> Row j x
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 Maybe x -> x -> Maybe x
forall {a}.
(Additive a, Multiplicative a) =>
Maybe a -> a -> Maybe a
(<*$) Maybe x -> Maybe x -> Maybe x
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
_  = Maybe a
forall a. Maybe a
Nothing
  (Just a
x) <*$ a
r = (a -> Bool) -> a -> Maybe a
forall a. (a -> Bool) -> a -> Maybe a
just (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.a -> Bool
forall a. Additive a => a -> Bool
isZero) (a
xa -> a -> a
forall 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 = (a -> Bool) -> a -> Maybe a
forall a. (a -> Bool) -> a -> Maybe a
just (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.a -> Bool
forall a. Additive a => a -> Bool
isZero) (a
aa -> a -> a
forall 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 = (x -> Row j x -> Maybe (Row j x))
-> i -> x -> Col i (Row j x) -> Col i (Row j x)
forall i s x.
Ord i =>
(s -> x -> Maybe x) -> i -> s -> Col i x -> Col i x
colScale x -> Row j x -> Maybe (Row j x)
forall {a} {j}. Distributive a => a -> Row j a -> Maybe (Row j a)
(*>) i
i (Inv x -> x
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 = (Row j a -> Bool) -> Row j a -> Maybe (Row j a)
forall a. (a -> Bool) -> a -> Maybe a
just (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (Row j a -> Bool) -> Row j a -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.Row j a -> Bool
forall j x. Row j x -> Bool
rowIsEmpty) (a
a a -> Row j a -> Row j 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
  = (Row j x -> Bool) -> Col i (Row j x) -> Col i (Row j x)
forall x i. (x -> Bool) -> Col i x -> Col i x
colFilter (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (Row j x -> Bool) -> Row j x -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.Row j x -> Bool
forall j x. Row j x -> Bool
rowIsEmpty) (Col i (Row j x) -> Col i (Row j x))
-> Col i (Row j x) -> Col i (Row j x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Row j x -> Row j x) -> Col i (Row j x) -> Col i (Row j x)
forall a b. (a -> b) -> Col i a -> Col i b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((x -> x -> Maybe x) -> j -> x -> Row j x -> Row j x
forall j x s.
Ord j =>
(x -> s -> Maybe x) -> j -> s -> Row j x -> Row j x
rowScale x -> x -> Maybe x
forall {a}. (Additive a, Multiplicative a) => a -> a -> Maybe a
(<*$) j
j (Inv x -> x
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 = (a -> Bool) -> a -> Maybe a
forall a. (a -> Bool) -> a -> Maybe a
just (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.a -> Bool
forall a. Additive a => a -> Bool
isZero) (a
xa -> a -> a
forall 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 = (Col i x -> x -> Maybe (Col i x))
-> j -> x -> Row j (Col i x) -> Row j (Col i x)
forall j x s.
Ord j =>
(x -> s -> Maybe x) -> j -> s -> Row j x -> Row j x
rowScale Col i x -> x -> Maybe (Col i x)
forall {a} {i}. Distributive a => Col i a -> a -> Maybe (Col i a)
(<*$) j
j (Inv x -> x
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 = (Col i a -> Bool) -> Col i a -> Maybe (Col i a)
forall a. (a -> Bool) -> a -> Maybe a
just (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (Col i a -> Bool) -> Col i a -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.Col i a -> Bool
forall i x. Col i x -> Bool
colIsEmpty) (Col i a
cl Col i a -> a -> Col i a
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) = (Maybe (Col i x) -> x -> Maybe (Col i x))
-> (Maybe (Col i x) -> Maybe (Col i x) -> Maybe (Col i x))
-> j
-> j
-> x
-> x
-> x
-> x
-> Row j (Col i x)
-> Row j (Col i x)
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 Maybe (Col i x) -> x -> Maybe (Col i x)
forall {a} {i}.
Distributive a =>
Maybe (Col i a) -> a -> Maybe (Col i a)
(<*$) Maybe (Col i x) -> Maybe (Col i x) -> Maybe (Col i x)
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
_   = Maybe (Col i a)
forall a. Maybe a
Nothing
  (Just Col i a
cl) <*$ a
a = (Col i a -> Bool) -> Col i a -> Maybe (Col i a)
forall a. (a -> Bool) -> a -> Maybe a
just (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (Col i a -> Bool) -> Col i a -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.Col i a -> Bool
forall i x. Col i x -> Bool
colIsEmpty) (Col i a
cl Col i a -> a -> Col i a
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 = (Col i a -> Bool) -> Col i a -> Maybe (Col i a)
forall a. (a -> Bool) -> a -> Maybe a
just (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (Col i a -> Bool) -> Col i a -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.Col i a -> Bool
forall i x. Col i x -> Bool
colIsEmpty) (Col i a
a Col i a -> Col i a -> Col i 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 Col N (Row N x) -> Permutation N -> Col N (Row N x)
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   = N -> Inv x -> Col N (Row N x) -> Col N (Row N x)
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 = N -> N -> GL2 x -> Col N (Row N x) -> Col N (Row N x)
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) = (Row N x -> Row N x) -> Col N (Row N x) -> Col N (Row N x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Row N x -> Permutation N -> Row N x
forall f x. Opr f x => x -> f -> x
<*Permutation N
p') Col N (Row N x)
rws where p' :: Permutation N
p' = Permutation N -> Permutation N
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)   = N -> Inv x -> Col N (Row N x) -> Col N (Row N x)
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) = N -> N -> GL2 x -> Col N (Row N x) -> Col N (Row N x)
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 Row N (Col N x) -> Permutation N -> Row N (Col N x)
forall f x. Opr f x => x -> f -> x
<* Permutation N
p' where p' :: Permutation N
p' = Permutation N -> Permutation N
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)   = N -> Inv x -> Row N (Col N x) -> Row N (Col N x)
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) = N -> N -> GL2 x -> Row N (Col N x) -> Row N (Col N x)
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
(ColTrafo x -> ColTrafo x -> Bool)
-> (ColTrafo x -> ColTrafo x -> Bool) -> Eq (ColTrafo x)
forall x. Oriented x => ColTrafo x -> ColTrafo x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: ColTrafo x -> ColTrafo x -> Bool
Eq,Int -> ColTrafo x -> ShowS
[ColTrafo x] -> ShowS
ColTrafo x -> String
(Int -> ColTrafo x -> ShowS)
-> (ColTrafo x -> String)
-> ([ColTrafo x] -> ShowS)
-> Show (ColTrafo x)
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
$cshowsPrec :: forall x. Oriented x => Int -> ColTrafo x -> ShowS
showsPrec :: Int -> ColTrafo x -> ShowS
$cshow :: forall x. Oriented x => ColTrafo x -> String
show :: ColTrafo x -> String
$cshowList :: forall x. Oriented x => [ColTrafo x] -> ShowS
showList :: [ColTrafo x] -> ShowS
Show,ColTrafo x -> Statement
(ColTrafo x -> Statement) -> Validable (ColTrafo x)
forall x. Oriented x => ColTrafo x -> Statement
forall a. (a -> Statement) -> Validable a
$cvalid :: forall x. Oriented x => ColTrafo x -> Statement
valid :: ColTrafo x -> Statement
Validable, Oriented (ColTrafo x)
Point (ColTrafo x) -> ColTrafo x
Oriented (ColTrafo x) =>
(Point (ColTrafo x) -> ColTrafo x)
-> (ColTrafo x -> ColTrafo x -> ColTrafo x)
-> (ColTrafo x -> N -> ColTrafo x)
-> Multiplicative (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
$cone :: forall x. Oriented x => Point (ColTrafo x) -> ColTrafo x
one :: Point (ColTrafo x) -> ColTrafo x
$c* :: forall x. Oriented x => ColTrafo x -> ColTrafo x -> ColTrafo x
* :: ColTrafo x -> ColTrafo x -> ColTrafo x
$cnpower :: forall x. Oriented x => ColTrafo x -> N -> ColTrafo x
npower :: ColTrafo x -> N -> ColTrafo x
Multiplicative, Multiplicative (ColTrafo x)
Multiplicative (ColTrafo x) =>
(ColTrafo x -> Solver (ColTrafo x))
-> (ColTrafo x -> ColTrafo x)
-> (ColTrafo x -> Bool)
-> (ColTrafo x -> Z -> ColTrafo x)
-> Invertible (ColTrafo x)
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
$ctryToInvert :: forall x. Oriented x => ColTrafo x -> Solver (ColTrafo x)
tryToInvert :: ColTrafo x -> Solver (ColTrafo x)
$cinvert :: forall x. Oriented x => ColTrafo x -> ColTrafo x
invert :: ColTrafo x -> ColTrafo x
$cisInvertible :: forall x. Oriented x => ColTrafo x -> Bool
isInvertible :: ColTrafo x -> Bool
$czpower :: forall x. Oriented x => ColTrafo x -> Z -> ColTrafo x
zpower :: ColTrafo x -> Z -> ColTrafo x
Invertible, Invertible (ColTrafo x)
Invertible (ColTrafo x) => Cayleyan (ColTrafo x)
forall x. Oriented x => Invertible (ColTrafo x)
forall c. Invertible c => Cayleyan c
Cayleyan)

type instance Point (ColTrafo x) = Dim x (Point x)
instance Oriented x => ShowPoint (ColTrafo x)
instance Oriented x => EqPoint (ColTrafo x)
instance Oriented x => ValidablePoint (ColTrafo x)
instance Oriented x => TypeablePoint (ColTrafo x)

instance Oriented x => Oriented (ColTrafo x) where
  orientation :: ColTrafo x -> Orientation (Point (ColTrafo x))
orientation (ColTrafo GLT x
t) = GLT x -> Orientation (Point (GLT x))
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 = GLT x -> ColTrafo x
forall x. GLT x -> ColTrafo x
ColTrafo (GLT x
tGLT x -> Exponent (GLT x) -> GLT x
forall f. Exponential f => f -> Exponent f -> f
^Exponent (GLT x)
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)
Dim x (Point x)
d Dim x (Point x) -> Dim x (Point x) -> Bool
forall a. Eq a => a -> a -> Bool
== Dim x (Point x)
c    = Dim x (Point x) -> Dim x (Point x) -> Entries N N x -> Matrix x
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim x (Point x)
r (GLT x -> Point (GLT x)
forall q. Oriented q => q -> Point q
start GLT x
t) (Row N (Col N x) -> Entries N N x
forall i j x. (Ord i, Ord j) => Row j (Col i x) -> Entries i j x
rcets (Entries N N x -> Row N (Col N x)
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)
<| GLT x -> ProductForm N (Transformation 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 = ArithmeticException -> Matrix x
forall a e. Exception e => e -> a
throw ArithmeticException
NotApplicable
    where d :: Point (GLT x)
d    = GLT x -> Point (GLT x)
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)
(<|) = N
-> (Row N (Col N x) -> Transformation x -> Row N (Col N x))
-> 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 Row N (Col N x) -> Transformation x -> Row N (Col N x)
forall x. Row N (Col N x) -> Transformation x -> Row N (Col N x)
rcTrafoCols
          n :: N
n    = N
10 N -> N -> N
forall a. Ord a => a -> a -> a
`max` (Dim x (Point x) -> N
forall x. LengthN x => x -> N
lengthN Point (GLT x)
Dim x (Point x)
d N -> N -> N
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 x = RowTrafo (GLT x)
  deriving (RowTrafo x -> RowTrafo x -> Bool
(RowTrafo x -> RowTrafo x -> Bool)
-> (RowTrafo x -> RowTrafo x -> Bool) -> Eq (RowTrafo x)
forall x. Oriented x => RowTrafo x -> RowTrafo x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall x. Oriented x => RowTrafo x -> RowTrafo x -> Bool
== :: RowTrafo x -> RowTrafo x -> Bool
$c/= :: forall x. Oriented x => RowTrafo x -> RowTrafo x -> Bool
/= :: RowTrafo x -> RowTrafo x -> Bool
Eq,Int -> RowTrafo x -> ShowS
[RowTrafo x] -> ShowS
RowTrafo x -> String
(Int -> RowTrafo x -> ShowS)
-> (RowTrafo x -> String)
-> ([RowTrafo x] -> ShowS)
-> Show (RowTrafo x)
forall x. Oriented x => Int -> RowTrafo x -> ShowS
forall x. Oriented x => [RowTrafo x] -> ShowS
forall x. Oriented x => RowTrafo x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall x. Oriented x => Int -> RowTrafo x -> ShowS
showsPrec :: Int -> RowTrafo x -> ShowS
$cshow :: forall x. Oriented x => RowTrafo x -> String
show :: RowTrafo x -> String
$cshowList :: forall x. Oriented x => [RowTrafo x] -> ShowS
showList :: [RowTrafo x] -> ShowS
Show,RowTrafo x -> Statement
(RowTrafo x -> Statement) -> Validable (RowTrafo x)
forall x. Oriented x => RowTrafo x -> Statement
forall a. (a -> Statement) -> Validable a
$cvalid :: forall x. Oriented x => RowTrafo x -> Statement
valid :: RowTrafo x -> Statement
Validable, Oriented (RowTrafo x)
Point (RowTrafo x) -> RowTrafo x
Oriented (RowTrafo x) =>
(Point (RowTrafo x) -> RowTrafo x)
-> (RowTrafo x -> RowTrafo x -> RowTrafo x)
-> (RowTrafo x -> N -> RowTrafo x)
-> Multiplicative (RowTrafo x)
RowTrafo x -> N -> RowTrafo x
RowTrafo x -> RowTrafo x -> RowTrafo x
forall x. Oriented x => Oriented (RowTrafo x)
forall x. Oriented x => Point (RowTrafo x) -> RowTrafo x
forall x. Oriented x => RowTrafo x -> N -> RowTrafo x
forall x. Oriented x => RowTrafo x -> RowTrafo x -> RowTrafo x
forall c.
Oriented c =>
(Point c -> c)
-> (c -> c -> c) -> (c -> N -> c) -> Multiplicative c
$cone :: forall x. Oriented x => Point (RowTrafo x) -> RowTrafo x
one :: Point (RowTrafo x) -> RowTrafo x
$c* :: forall x. Oriented x => RowTrafo x -> RowTrafo x -> RowTrafo x
* :: RowTrafo x -> RowTrafo x -> RowTrafo x
$cnpower :: forall x. Oriented x => RowTrafo x -> N -> RowTrafo x
npower :: RowTrafo x -> N -> RowTrafo x
Multiplicative, Multiplicative (RowTrafo x)
Multiplicative (RowTrafo x) =>
(RowTrafo x -> Solver (RowTrafo x))
-> (RowTrafo x -> RowTrafo x)
-> (RowTrafo x -> Bool)
-> (RowTrafo x -> Z -> RowTrafo x)
-> Invertible (RowTrafo x)
RowTrafo x -> Bool
RowTrafo x -> Solver (RowTrafo x)
RowTrafo x -> RowTrafo x
RowTrafo x -> Z -> RowTrafo x
forall x. Oriented x => Multiplicative (RowTrafo x)
forall x. Oriented x => RowTrafo x -> Bool
forall x. Oriented x => RowTrafo x -> Solver (RowTrafo x)
forall x. Oriented x => RowTrafo x -> RowTrafo x
forall x. Oriented x => RowTrafo x -> Z -> RowTrafo x
forall c.
Multiplicative c =>
(c -> Solver c)
-> (c -> c) -> (c -> Bool) -> (c -> Z -> c) -> Invertible c
$ctryToInvert :: forall x. Oriented x => RowTrafo x -> Solver (RowTrafo x)
tryToInvert :: RowTrafo x -> Solver (RowTrafo x)
$cinvert :: forall x. Oriented x => RowTrafo x -> RowTrafo x
invert :: RowTrafo x -> RowTrafo x
$cisInvertible :: forall x. Oriented x => RowTrafo x -> Bool
isInvertible :: RowTrafo x -> Bool
$czpower :: forall x. Oriented x => RowTrafo x -> Z -> RowTrafo x
zpower :: RowTrafo x -> Z -> RowTrafo x
Invertible, Invertible (RowTrafo x)
Invertible (RowTrafo x) => Cayleyan (RowTrafo x)
forall x. Oriented x => Invertible (RowTrafo x)
forall c. Invertible c => Cayleyan c
Cayleyan)

type instance Point (RowTrafo x) = Dim x (Point x)
instance Oriented x => ShowPoint (RowTrafo x)
instance Oriented x => EqPoint (RowTrafo x)
instance Oriented x => ValidablePoint (RowTrafo x)
instance Oriented x => TypeablePoint (RowTrafo x)

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

instance Oriented x => Exponential (RowTrafo x) where
  type Exponent (RowTrafo x) = Z
  RowTrafo GLT x
t ^ :: RowTrafo x -> Exponent (RowTrafo x) -> RowTrafo x
^ Exponent (RowTrafo x)
z = GLT x -> RowTrafo x
forall x. GLT x -> RowTrafo x
RowTrafo (GLT x
tGLT x -> Exponent (GLT x) -> GLT x
forall f. Exponential f => f -> Exponent f -> f
^Exponent (GLT x)
Exponent (RowTrafo x)
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)
Dim x (Point x)
d Dim x (Point x) -> Dim x (Point x) -> Bool
forall a. Eq a => a -> a -> Bool
== Dim x (Point x)
r    = Dim x (Point x) -> Dim x (Point x) -> Entries N N x -> Matrix x
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix (GLT x -> Point (GLT x)
forall q. Oriented q => q -> Point q
end GLT x
t) Dim x (Point x)
c (Entries N N x -> Matrix x) -> Entries N N x -> Matrix x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Col N (Row N x) -> Entries N N x
forall i j x. Col i (Row j x) -> Entries i j x
crets (GLT x -> ProductForm N (Transformation x)
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)
|> Entries N 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 = ArithmeticException -> Matrix x
forall a e. Exception e => e -> a
throw ArithmeticException
NotApplicable
    where d :: Point (GLT x)
d = GLT x -> Point (GLT x)
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)
(|>) = N
-> (Transformation x -> Col N (Row N x) -> Col N (Row N x))
-> 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 Transformation x -> Col N (Row N x) -> Col N (Row N x)
forall x. Transformation x -> Col N (Row N x) -> Col N (Row N x)
crTrafoRows
          n :: N
n    = N
10 N -> N -> N
forall a. Ord a => a -> a -> a
`max` (Dim x (Point x) -> N
forall x. LengthN x => x -> N
lengthN Point (GLT x)
Dim x (Point x)
d N -> N -> N
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
(DiagonalForm k -> DiagonalForm k -> Bool)
-> (DiagonalForm k -> DiagonalForm k -> Bool)
-> Eq (DiagonalForm k)
forall k. Oriented k => DiagonalForm k -> DiagonalForm k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: DiagonalForm k -> DiagonalForm k -> Bool
Eq,Int -> DiagonalForm k -> ShowS
[DiagonalForm k] -> ShowS
DiagonalForm k -> String
(Int -> DiagonalForm k -> ShowS)
-> (DiagonalForm k -> String)
-> ([DiagonalForm k] -> ShowS)
-> Show (DiagonalForm k)
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
$cshowsPrec :: forall k. Oriented k => Int -> DiagonalForm k -> ShowS
showsPrec :: Int -> DiagonalForm k -> ShowS
$cshow :: forall k. Oriented k => DiagonalForm k -> String
show :: DiagonalForm k -> String
$cshowList :: forall k. Oriented k => [DiagonalForm k] -> ShowS
showList :: [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 [ ([k], RowTrafo k, ColTrafo k) -> Statement
forall a. Validable a => a -> Statement
valid ([k]
ds,RowTrafo k
rt,ColTrafo k
ct)
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>:
            ([k] -> N
forall x. LengthN x => x -> N
lengthN [k]
ds N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<= N -> N -> N
forall a. Ord a => a -> a -> a
min (Dim k (Point k) -> N
forall x. LengthN x => x -> N
lengthN (RowTrafo k -> Point (RowTrafo k)
forall q. Oriented q => q -> Point q
start RowTrafo k
rt)) (Dim k (Point k) -> N
forall x. LengthN x => x -> N
lengthN (ColTrafo k -> Point (ColTrafo k)
forall q. Oriented q => q -> Point q
end ColTrafo k
ct)))
              Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[ String
"lengthN ds"String -> String -> Parameter
:=Int -> String
forall a. Show a => a -> String
show ([k] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [k]
ds)
                       , String
"lengthN (start rt)"String -> String -> Parameter
:= N -> String
forall a. Show a => a -> String
show (Dim k (Point k) -> N
forall x. LengthN x => x -> N
lengthN (RowTrafo k -> Point (RowTrafo k)
forall q. Oriented q => q -> Point q
start RowTrafo k
rt))
                       , String
"lengthN (end ct)"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show (Dim k (Point k) -> N
forall x. LengthN x => x -> N
lengthN (ColTrafo k -> Point (ColTrafo k)
forall q. Oriented q => q -> Point q
end ColTrafo k
ct))
                       ]
        , String -> Label
Label String
"2"
            Label -> Statement -> Statement
:<=>: ([Bool] -> Bool
forall b. Boolean b => [b] -> b
and ([Bool] -> Bool) -> [Bool] -> Bool
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (k -> Bool) -> [k] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (k -> Bool) -> k -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.k -> Bool
forall a. Additive a => a -> Bool
isZero) [k]
ds) Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"ds"String -> String -> Parameter
:=[k] -> String
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'RowTrafo k -> Matrix k -> Matrix k
forall f x. Opl f x => f -> x -> x
*>Matrix k
dm)Matrix k -> ColTrafo k -> Matrix k
forall f x. Opr f x => x -> f -> x
<*ColTrafo k
ct' where
  rt' :: RowTrafo k
rt' = RowTrafo k -> RowTrafo k
forall c. Invertible c => c -> c
invert RowTrafo k
rt
  ct' :: ColTrafo k
ct' = ColTrafo k -> ColTrafo k
forall c. Invertible c => c -> c
invert ColTrafo k
ct
  dm :: Matrix k
dm = Dim' k -> Dim' k -> [k] -> Matrix k
forall x. Additive x => Dim' x -> Dim' x -> [x] -> Matrix x
diagonal (RowTrafo k -> Point (RowTrafo k)
forall q. Oriented q => q -> Point q
start RowTrafo k
rt') (ColTrafo k -> Point (ColTrafo k)
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
[DiagonalFormStrictPositive k] -> ShowS
DiagonalFormStrictPositive k -> String
(Int -> DiagonalFormStrictPositive k -> ShowS)
-> (DiagonalFormStrictPositive k -> String)
-> ([DiagonalFormStrictPositive k] -> ShowS)
-> Show (DiagonalFormStrictPositive k)
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
$cshowsPrec :: forall k.
Oriented k =>
Int -> DiagonalFormStrictPositive k -> ShowS
showsPrec :: Int -> DiagonalFormStrictPositive k -> ShowS
$cshow :: forall k. Oriented k => DiagonalFormStrictPositive k -> String
show :: DiagonalFormStrictPositive k -> String
$cshowList :: forall k. Oriented k => [DiagonalFormStrictPositive k] -> ShowS
showList :: [DiagonalFormStrictPositive k] -> ShowS
Show,DiagonalFormStrictPositive k
-> DiagonalFormStrictPositive k -> Bool
(DiagonalFormStrictPositive k
 -> DiagonalFormStrictPositive k -> Bool)
-> (DiagonalFormStrictPositive k
    -> DiagonalFormStrictPositive k -> Bool)
-> Eq (DiagonalFormStrictPositive k)
forall k.
Oriented k =>
DiagonalFormStrictPositive k
-> DiagonalFormStrictPositive k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: 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 [ DiagonalForm k -> Statement
forall a. Validable a => a -> Statement
valid DiagonalForm k
f
          , N -> [k] -> Statement
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 [ (a
forall r. Semiring r => r
rZero a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
d)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(d,i)"String -> String -> Parameter
:=(a, t) -> String
forall a. Show a => a -> String
show (a
d,t
i)]
                       , t -> [a] -> Statement
vld (t -> t
forall a. Enum a => a -> a
succ t
i) [a]
ds
                       ]
                   
-- instance Number k => Entity (DiagonalFormStrictPositive k)