{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}

-- |
-- Module      : OAlg.AbelianGroup.Free.SmithNormalForm
-- Description : diagonal and Smith Normal Form for matrices over integers
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- diagonal and Smith Normal Form for 'Z'-matrices.
module OAlg.AbelianGroup.Free.SmithNormalForm
  (
    -- * Diagonal Form
    zmxDiagonalForm

    -- * Smith Normal Form
  , smithNormalForm, smithNormalForm'
  , zmxDiagonalFormStrictPositive
  , SmithNormalForm(..), snfDiagonalForm

    -- * Proposition
  , prpDiagonalFormZ
  )
  where

import Control.Monad
import Data.List ((++),repeat,dropWhile)

import OAlg.Prelude

import OAlg.Data.Canonical
import OAlg.Data.Constructable
import OAlg.Data.Reducible

import OAlg.Structure.Oriented
import OAlg.Structure.Additive
import OAlg.Structure.Multiplicative
import OAlg.Structure.Number
import OAlg.Structure.Ring

import OAlg.Entity.Product
import OAlg.Entity.Matrix
import OAlg.Entity.Sequence.Permutation
import OAlg.Entity.Sequence.PSequence

import OAlg.AbelianGroup.Euclid

--------------------------------------------------------------------------------
-- crDiagonalForm -

type TPRows a = ProductForm Z (Transformation a)
type TPCols a = ProductForm Z (Transformation a)
type NF a     = ([a], TPRows a, TPCols a)

-- | reducing a matrix over 'Z' to a diagonal matrix by applying elements of @'GLT' 'Z'@.
-- The entries of the diagonal may not be successively divisible!
crDiagonalForm :: (i ~ N, j ~ N) => Dim Z () -> Dim Z () -> Col i (Row j Z) -> NF Z
crDiagonalForm :: forall i j.
(i ~ N, j ~ N) =>
Dim Z () -> Dim Z () -> Col i (Row j Z) -> NF Z
crDiagonalForm = i -> Dim' Z -> Dim' Z -> Col i (Row j Z) -> NF Z
forall i j.
(i ~ N, j ~ N) =>
i -> Dim' Z -> Dim' Z -> Col i (Row j Z) -> NF Z
dnf' i
0

--------------------------------------------------------------------------------
-- dnf -

dnfis :: Eq j => j -> Col i (Row j Z) -> [(Z,i)]
dnfis :: forall j i. Eq j => j -> Col i (Row j Z) -> [(Z, i)]
dnfis j
j = Col i Z -> [(Z, i)]
forall i x. Col i x -> [(x, i)]
colxs (Col i Z -> [(Z, i)])
-> (Col i (Row j Z) -> Col i Z) -> Col i (Row j Z) -> [(Z, i)]
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 Z -> Col i Z
forall i x. Col i x -> Col i x
colTail (Col i Z -> Col i Z)
-> (Col i (Row j Z) -> Col i Z) -> Col i (Row j Z) -> Col i Z
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
. j -> Col i (Row j Z) -> Col i Z
forall j i a. Eq j => j -> Col i (Row j a) -> Col i a
crHeadColAt j
j

dnfjs :: Eq i => i -> Col i (Row j Z) -> [(Z,j)]
dnfjs :: forall i j. Eq i => i -> Col i (Row j Z) -> [(Z, j)]
dnfjs i
i = Row j Z -> [(Z, j)]
forall j x. Row j x -> [(x, j)]
rowxs (Row j Z -> [(Z, j)])
-> (Col i (Row j Z) -> Row j Z) -> Col i (Row j Z) -> [(Z, j)]
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 Z -> Row j Z
forall j x. Row j x -> Row j x
rowTail (Row j Z -> Row j Z)
-> (Col i (Row j Z) -> Row j Z) -> Col i (Row j Z) -> Row j Z
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
. i -> Col i (Row j Z) -> Row j Z
forall i j a. Eq i => i -> Col i (Row j a) -> Row j a
crHeadRowAt i
i


-- | transformation by the given offset to diagonal form where the entries of the
-- diagonal may not be successively divisible.
--
-- __Properties__ Let @r@ be in 'N', @n@, @m@ in @'Dim'' 'Z'@ and @rws@ be in
-- @'Col' i ('Row' j 'Z')@ where for all entries @(x,(i,j)@ in @rws@ holds
--
-- (1) @x '/= 0@.
--
-- (2) @r '<=' i@ and @r '<=' j@.
--
-- then holds: Let @(ds,a',b') = 'dnf'' r n m rws@ in
--
-- (1) @0 < d@ for all @d@ in @ds@.
--
-- (2) @(a 'OAlg.Structure.Operational.*>' 'Matrix' n m ('crets' rws))
-- 'OAlg.Structure.Operational.<*' b '==' 'diagonal'' r n m ds@ where
-- @a' = 'RowTrafo' ('make' a' :: 'GLT' 'Z')@ and @b = 'ColTrafo' ('make' b :: 'GLT' 'Z')@.
dnf' :: (i ~ N, j ~ N) => i -> Dim' Z -> Dim' Z -> Col i (Row j Z) -> NF Z
dnf' :: forall i j.
(i ~ N, j ~ N) =>
i -> Dim' Z -> Dim' Z -> Col i (Row j Z) -> NF Z
dnf' i
r Dim' Z
n Dim' Z
m Col i (Row j Z)
rws = Dim Z () -> Dim Z () -> N -> Col i (Row j Z) -> NF Z -> NF Z
forall i j.
(i ~ N, j ~ N) =>
Dim Z () -> Dim Z () -> N -> Col i (Row j Z) -> NF Z -> NF Z
dnf1 Dim Z ()
Dim' Z
n Dim Z ()
Dim' Z
m i
N
r Col i (Row j Z)
rws ([],Point (Transformation Z) -> ProductForm Z (Transformation Z)
forall r a. Point a -> ProductForm r a
One Point (Transformation Z)
Dim' Z
n,Point (Transformation Z) -> ProductForm Z (Transformation Z)
forall r a. Point a -> ProductForm r a
One Point (Transformation Z)
Dim' Z
m)

-- | pre:
--
--   (1) for all @i@, @j@ in @rws@ holds: @r '<=' i@ and @r '<=' j@. 
dnf1 :: (i ~ N, j ~ N) => Dim Z () -> Dim Z () -> N -> Col i (Row j Z) -> NF Z -> NF Z
dnf1 :: forall i j.
(i ~ N, j ~ N) =>
Dim Z () -> Dim Z () -> N -> Col i (Row j Z) -> NF Z -> NF Z
dnf1 Dim Z ()
dr Dim Z ()
dc N
r Col i (Row j Z)
rws NF Z
res = if Col i (Row j Z) -> Bool
forall i x. Col i x -> Bool
colIsEmpty Col i (Row j Z)
rws
  then NF Z
res
  else Dim Z ()
-> Dim Z ()
-> N
-> Col i (Row j Z)
-> [(Z, i)]
-> [(Z, i)]
-> NF Z
-> NF Z
forall i j.
(i ~ N, j ~ N) =>
Dim Z ()
-> Dim Z ()
-> N
-> Col i (Row j Z)
-> [(Z, i)]
-> [(Z, i)]
-> NF Z
-> NF Z
dnf3 Dim Z ()
dr Dim Z ()
dc N
r Col i (Row j Z)
rws' (N -> Col i (Row N Z) -> [(Z, i)]
forall j i. Eq j => j -> Col i (Row j Z) -> [(Z, i)]
dnfis N
r Col i (Row j Z)
Col i (Row N Z)
rws') (N -> Col N (Row i Z) -> [(Z, i)]
forall i j. Eq i => i -> Col i (Row j Z) -> [(Z, j)]
dnfjs N
r Col i (Row j Z)
Col N (Row i Z)
rws') NF Z
res' where
    (Col i (Row j Z)
rws',NF Z
res') = Dim Z ()
-> Dim Z ()
-> N
-> Col i (Row j Z)
-> NF Z
-> (Col i (Row j Z), NF Z)
forall i j.
(i ~ N, j ~ N) =>
Dim Z ()
-> Dim Z ()
-> N
-> Col i (Row j Z)
-> NF Z
-> (Col i (Row j Z), NF Z)
dnf2 Dim Z ()
dr Dim Z ()
dc N
r Col i (Row j Z)
rws NF Z
res

-- | swap a non zero entry to the position @(r,r)@ and scale it to be strict positive.
--
-- pre:
--
-- (1) @rws@ is not empty.
--
-- (2) for all @i@, @j@ in @rws@ holds: @r '<=' i@ and @r '<=' j@.
--
-- post:
--
-- (1) the entry @0 '<' rws' r r@.
dnf2 :: (i ~ N, j ~ N)
  => Dim Z () -> Dim Z () -> N -> Col i (Row j Z) -> NF Z -> (Col i (Row j Z),NF Z)
dnf2 :: forall i j.
(i ~ N, j ~ N) =>
Dim Z ()
-> Dim Z ()
-> N
-> Col i (Row j Z)
-> NF Z
-> (Col i (Row j Z), NF Z)
dnf2 Dim Z ()
dr Dim Z ()
dc N
r Col i (Row j Z)
rws ([Z]
ds,ProductForm Z (Transformation Z)
trs,ProductForm Z (Transformation Z)
tcs) = (Col i (Row j Z)
Col N (Row N Z)
rws',([Z]
ds,ProductForm Z (Transformation Z)
trs',ProductForm Z (Transformation Z)
tcs')) where
  (Row j Z
rw,i
i) = Col i (Row j Z) -> (Row j Z, i)
forall i x. Col i x -> (x, i)
colHead Col i (Row j Z)
rws
  (Z
a,j
j)  = Row j Z -> (Z, j)
forall j x. Row j x -> (x, j)
rowHead Row j Z
rw
  sa :: Z
sa     = Z -> Z
forall r. Number r => r -> r
signum Z
a

  rws' :: Col N (Row N Z)
rws'   = (GLT Z
tr GLT Z -> Col N (Row N Z) -> Col N (Row N Z)
forall {a} {x}.
Embeddable a (ProductForm N (Transformation x)) =>
a -> Col N (Row N x) -> Col N (Row N x)
|> Col i (Row j Z)
Col N (Row N Z)
rws) Col N (Row N Z) -> GLT Z -> Col N (Row N Z)
forall {a} {x}.
Embeddable a (ProductForm N (Transformation x)) =>
Col N (Row N x) -> a -> Col N (Row N x)
<| GLT Z
tc where
    a
t |> :: a -> Col N (Row N x) -> Col N (Row N x)
|> Col N (Row N x)
rws = (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. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl 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 (a -> ProductForm N (Transformation x)
forall a b. Embeddable a b => a -> b
inj a
t) Col N (Row N x)
rws
    Col N (Row N x)
rws <| :: Col N (Row N x) -> a -> Col N (Row N x)
<| a
t = (Col N (Row N x) -> Transformation x -> Col N (Row N x))
-> Col N (Row N x)
-> ProductForm N (Transformation x)
-> Col N (Row N x)
forall x t. (x -> t -> x) -> x -> ProductForm N t -> x
prfopr Col N (Row N x) -> Transformation x -> Col N (Row N x)
forall x. Col N (Row N x) -> Transformation x -> Col N (Row N x)
crTrafoCols Col N (Row N x)
rws (a -> ProductForm N (Transformation x)
forall a b. Embeddable a b => a -> b
inj a
t)
    -- tr and tc are reduced and hence alle exponentes are bigger then zero!
    
  tr :: GLT Z
tr     = Form (GLT Z) -> GLT Z
forall x. Constructable x => Form x -> x
make (Transformation Z -> ProductForm Z (Transformation Z)
forall r a. a -> ProductForm r a
P (Dim' Z -> N -> Inv Z -> Transformation Z
forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim Z ()
Dim' Z
dr N
r (Z -> Z -> Inv Z
forall c. c -> c -> Inv c
Inv Z
sa Z
sa)) ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* Transformation Z -> ProductForm Z (Transformation Z)
forall r a. a -> ProductForm r a
P (Dim' Z -> Dim' Z -> Permutation N -> Transformation Z
forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim Z ()
Dim' Z
dr Dim Z ()
Dim' Z
dr (N -> N -> Permutation N
forall i. (Entity i, Ord i) => i -> i -> Permutation i
swap N
r i
N
i))) :: GLT Z
  tc :: GLT Z
tc     = Form (GLT Z) -> GLT Z
forall x. Constructable x => Form x -> x
make (Transformation Z -> ProductForm Z (Transformation Z)
forall r a. a -> ProductForm r a
P (Dim' Z -> Dim' Z -> Permutation N -> Transformation Z
forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim Z ()
Dim' Z
dc Dim Z ()
Dim' Z
dc (N -> N -> Permutation N
forall i. (Entity i, Ord i) => i -> i -> Permutation i
swap N
r j
N
j))) :: GLT Z
  trs' :: ProductForm Z (Transformation Z)
trs'   = GLT Z -> Form (GLT Z)
forall x. Exposable x => x -> Form x
form GLT Z
tr ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm Z (Transformation Z)
trs
  tcs' :: ProductForm Z (Transformation Z)
tcs'   = ProductForm Z (Transformation Z)
tcs ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* GLT Z -> Form (GLT Z)
forall x. Exposable x => x -> Form x
form GLT Z
tc


-- | @gcd@ of @a@ and @b@ with the appropriate row transformations to eliminate @b@.
--
-- pre: @0 < a@, @k < l@.
tRows :: i ~ N => Dim Z () -> (Z,i) -> (Z,i) -> (Z,TPRows Z)
tRows :: forall i.
(i ~ N) =>
Dim Z ()
-> (Z, i) -> (Z, i) -> (Z, ProductForm Z (Transformation Z))
tRows Dim Z ()
d (Z
a,i
k) (Z
b,i
l) = Z
-> Z
-> ProductForm Z (Transformation Z)
-> (Z, ProductForm Z (Transformation Z))
trws Z
a Z
b (Point (Transformation Z) -> ProductForm Z (Transformation Z)
forall r a. Point a -> ProductForm r a
One Point (Transformation Z)
Dim Z ()
d) where
  trws :: Z
-> Z
-> ProductForm Z (Transformation Z)
-> (Z, ProductForm Z (Transformation Z))
trws Z
a Z
b ProductForm Z (Transformation Z)
ts | Z
m Z -> Z -> Bool
forall a. Eq a => a -> a -> Bool
== Z
0 = (Z
a,Transformation Z -> ProductForm Z (Transformation Z)
forall r a. a -> ProductForm r a
P (Dim' Z -> N -> N -> GL2 Z -> Transformation Z
forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim Z ()
Dim' Z
d i
N
k i
N
l (Z -> Z -> Z -> Z -> GL2 Z
forall x. x -> x -> x -> x -> GL2 x
GL2 Z
1 Z
0 (-Z
q) Z
1))ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*ProductForm Z (Transformation Z)
ts) where
    (Z
q,Z
m) = Z
b Z -> Z -> (Z, Z)
forall a. Integral a => a -> a -> (a, a)
`divMod` Z
a

  trws Z
a Z
b ProductForm Z (Transformation Z)
ts = Z
-> Z
-> ProductForm Z (Transformation Z)
-> (Z, ProductForm Z (Transformation Z))
trws (N -> Z
forall a b. Embeddable a b => a -> b
inj N
g) (Z
vZ -> Z -> Z
forall c. Multiplicative c => c -> c -> c
*Z
b Z -> Z -> Z
forall a. Abelian a => a -> a -> a
- Z
uZ -> Z -> Z
forall c. Multiplicative c => c -> c -> c
*Z
a) (ProductForm Z (Transformation Z)
trProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*ProductForm Z (Transformation Z)
ts) where
    (N
g,Z
s,Z
t) = Z -> Z -> (N, Z, Z)
euclid Z
a Z
b
    (N
_,Z
u,Z
v) = Z -> Z -> (N, Z, Z)
euclid Z
t Z
s -- because g is gcd it follows that gcd s t == 1
    tr :: ProductForm Z (Transformation Z)
tr = Transformation Z -> ProductForm Z (Transformation Z)
forall r a. a -> ProductForm r a
P (Transformation Z -> ProductForm Z (Transformation Z))
-> Transformation Z -> ProductForm Z (Transformation Z)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Dim' Z -> N -> N -> GL2 Z -> Transformation Z
forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim Z ()
Dim' Z
d i
N
k i
N
l (Z -> Z -> Z -> Z -> GL2 Z
forall x. x -> x -> x -> x -> GL2 x
GL2 Z
s Z
t (-Z
u) Z
v)


-- | @gcd@ of @a@ and @b@ with the appropriate column transformation to eliminate @b@.
--
-- pre: @0 < a@, @k < l@.
tCols :: j ~ N => Dim Z () -> (Z,j) -> (Z,j) -> (Z,TPCols Z)
tCols :: forall i.
(i ~ N) =>
Dim Z ()
-> (Z, i) -> (Z, i) -> (Z, ProductForm Z (Transformation Z))
tCols Dim Z ()
d (Z, j)
ak (Z, j)
bl = (Z
g,ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r. TransposableDistributive r => GLTForm r -> GLTForm r
gltfTrsp ProductForm Z (Transformation Z)
tr) where
  (Z
g,ProductForm Z (Transformation Z)
tr) = Dim Z ()
-> (Z, j) -> (Z, j) -> (Z, ProductForm Z (Transformation Z))
forall i.
(i ~ N) =>
Dim Z ()
-> (Z, i) -> (Z, i) -> (Z, ProductForm Z (Transformation Z))
tRows Dim Z ()
d (Z, j)
ak (Z, j)
bl


-- | eliminates all non zero entries in the @r@-th row and column
--
-- pre:
--
-- (1) the entry at @(r,r)@ is strict positive
--
-- (1) @is@ are the row numbers of @rws@ with non zero entries at the column @r@
-- with @r '<' i@ for all @i@ in @is@.
--
-- (1) @js@ are the column numbers of @rws@ with non zero entries at the row @r@
-- with @r '<' j@ for all @j@ in @js@.
--
-- post: all entries in the @r@-th row and column - except the one at position @(r,r)@ -
-- are zero (i.e. are eliminated).
dnf3 :: (i ~ N, j ~ N)
  => Dim Z () -> Dim Z () -> N -> Col i (Row j Z) -> [(Z,i)] -> [(Z,i)] -> NF Z -> NF Z
-- this algorithem terminates because in each step the number of primfactors of
-- the entry at postion (r,r) is strict decreasing!
dnf3 :: forall i j.
(i ~ N, j ~ N) =>
Dim Z ()
-> Dim Z ()
-> N
-> Col i (Row j Z)
-> [(Z, i)]
-> [(Z, i)]
-> NF Z
-> NF Z
dnf3 Dim Z ()
dr Dim Z ()
dc N
r Col i (Row j Z)
rws [] [] NF Z
res = (Z
dZ -> [Z] -> [Z]
forall a. a -> [a] -> [a]
:[Z]
ds,ProductForm Z (Transformation Z)
trs,ProductForm Z (Transformation Z)
tcs) where
  d :: Z
d            = (Z, N) -> Z
forall a b. (a, b) -> a
fst ((Z, N) -> Z) -> (Z, N) -> Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Row N Z -> (Z, N)
forall j x. Row j x -> (x, j)
rowHead (Row N Z -> (Z, N)) -> Row N Z -> (Z, N)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (Row j Z, i) -> Row N Z
(Row N Z, N) -> Row N Z
forall a b. (a, b) -> a
fst ((Row j Z, i) -> Row N Z) -> (Row j Z, i) -> Row N Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Col i (Row j Z) -> (Row j Z, i)
forall i x. Col i x -> (x, i)
colHead Col i (Row j Z)
rws
  ([Z]
ds,ProductForm Z (Transformation Z)
trs,ProductForm Z (Transformation Z)
tcs) = Dim Z () -> Dim Z () -> N -> Col i (Row j Z) -> NF Z -> NF Z
forall i j.
(i ~ N, j ~ N) =>
Dim Z () -> Dim Z () -> N -> Col i (Row j Z) -> NF Z -> NF Z
dnf1 Dim Z ()
dr Dim Z ()
dc (N
rN -> N -> N
forall a. Additive a => a -> a -> a
+N
1) (Col i (Row j Z) -> Col i (Row j Z)
forall i x. Col i x -> Col i x
colTail Col i (Row j Z)
rws) NF Z
res

-- eliminates the column
dnf3 Dim Z ()
dr Dim Z ()
dc N
r Col i (Row j Z)
rws cl :: [(Z, i)]
cl@((Z, i)
_:[(Z, i)]
_) [(Z, i)]
_ ([Z]
ds,ProductForm Z (Transformation Z)
trs,ProductForm Z (Transformation Z)
tcs)
  = Dim Z ()
-> Dim Z ()
-> N
-> Col N (Row N Z)
-> [(Z, N)]
-> [(Z, N)]
-> NF Z
-> NF Z
forall i j.
(i ~ N, j ~ N) =>
Dim Z ()
-> Dim Z ()
-> N
-> Col i (Row j Z)
-> [(Z, i)]
-> [(Z, i)]
-> NF Z
-> NF Z
dnf3 Dim Z ()
dr Dim Z ()
dc N
r Col N (Row N Z)
rws' [] (N -> Col N (Row N Z) -> [(Z, N)]
forall i j. Eq i => i -> Col i (Row j Z) -> [(Z, j)]
dnfjs N
r Col N (Row N Z)
rws') ([Z]
ds,GLT Z -> Form (GLT Z)
forall x. Exposable x => x -> Form x
form GLT Z
tr ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*ProductForm Z (Transformation Z)
trs,ProductForm Z (Transformation Z)
tcs) where
      a
t *> :: a -> Col N (Row N x) -> Col N (Row N x)
*> Col N (Row N x)
rws = (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. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl 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 (a -> ProductForm N (Transformation x)
forall a b. Embeddable a b => a -> b
inj a
t) Col N (Row N x)
rws
      rws' :: Col N (Row N Z)
rws' = GLT Z
tr GLT Z -> Col N (Row N Z) -> Col N (Row N Z)
forall {a} {x}.
Embeddable a (ProductForm N (Transformation x)) =>
a -> Col N (Row N x) -> Col N (Row N x)
*> Col i (Row j Z)
Col N (Row N Z)
rws
      a :: Z
a    = (Z, N) -> Z
forall a b. (a, b) -> a
fst ((Z, N) -> Z) -> (Z, N) -> Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Row N Z -> (Z, N)
forall j x. Row j x -> (x, j)
rowHead (Row N Z -> (Z, N)) -> Row N Z -> (Z, N)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (Row j Z, i) -> Row N Z
(Row N Z, N) -> Row N Z
forall a b. (a, b) -> a
fst ((Row j Z, i) -> Row N Z) -> (Row j Z, i) -> Row N Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Col i (Row j Z) -> (Row j Z, i)
forall i x. Col i x -> (x, i)
colHead Col i (Row j Z)
rws
      tr :: GLT Z
tr   = Form (GLT Z) -> GLT Z
ProductForm Z (Transformation Z) -> GLT Z
forall x. Constructable x => Form x -> x
make (ProductForm Z (Transformation Z) -> GLT Z)
-> ProductForm Z (Transformation Z) -> GLT Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N
-> Z
-> [(Z, N)]
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
elims N
r Z
a [(Z, i)]
[(Z, N)]
cl (Point (Transformation Z) -> ProductForm Z (Transformation Z)
forall r a. Point a -> ProductForm r a
One Point (Transformation Z)
Dim Z ()
dr) :: GLT Z

      elims :: N
-> Z
-> [(Z, N)]
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
elims N
_ Z
_ [] ProductForm Z (Transformation Z)
tr          = ProductForm Z (Transformation Z)
tr
      elims N
r Z
a ((Z
b,N
i):[(Z, N)]
bis) ProductForm Z (Transformation Z)
tr = N
-> Z
-> [(Z, N)]
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
elims N
r Z
a' [(Z, N)]
bis (ProductForm Z (Transformation Z)
tr' ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm Z (Transformation Z)
tr) where
        (Z
a',ProductForm Z (Transformation Z)
tr') = Dim Z ()
-> (Z, N) -> (Z, N) -> (Z, ProductForm Z (Transformation Z))
forall i.
(i ~ N) =>
Dim Z ()
-> (Z, i) -> (Z, i) -> (Z, ProductForm Z (Transformation Z))
tRows Dim Z ()
dr (Z
a,N
r) (Z
b,N
i) 

-- eliminates the row
dnf3 Dim Z ()
dr Dim Z ()
dc N
r Col i (Row j Z)
rws [(Z, i)]
_ rw :: [(Z, i)]
rw@((Z, i)
_:[(Z, i)]
_) ([Z]
ds,ProductForm Z (Transformation Z)
trs,ProductForm Z (Transformation Z)
tcs)
  = Dim Z ()
-> Dim Z ()
-> N
-> Col N (Row N Z)
-> [(Z, N)]
-> [(Z, N)]
-> NF Z
-> NF Z
forall i j.
(i ~ N, j ~ N) =>
Dim Z ()
-> Dim Z ()
-> N
-> Col i (Row j Z)
-> [(Z, i)]
-> [(Z, i)]
-> NF Z
-> NF Z
dnf3 Dim Z ()
dr Dim Z ()
dc N
r Col N (Row N Z)
rws' (N -> Col N (Row N Z) -> [(Z, N)]
forall j i. Eq j => j -> Col i (Row j Z) -> [(Z, i)]
dnfis N
r Col N (Row N Z)
rws') [] ([Z]
ds,ProductForm Z (Transformation Z)
trs,ProductForm Z (Transformation Z)
tcsProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* GLT Z -> Form (GLT Z)
forall x. Exposable x => x -> Form x
form GLT Z
tc) where
      Col N (Row N x)
rws <* :: Col N (Row N x) -> a -> Col N (Row N x)
<* a
t = (Col N (Row N x) -> Transformation x -> Col N (Row N x))
-> Col N (Row N x)
-> ProductForm N (Transformation x)
-> Col N (Row N x)
forall x t. (x -> t -> x) -> x -> ProductForm N t -> x
prfopr Col N (Row N x) -> Transformation x -> Col N (Row N x)
forall x. Col N (Row N x) -> Transformation x -> Col N (Row N x)
crTrafoCols Col N (Row N x)
rws (a -> ProductForm N (Transformation x)
forall a b. Embeddable a b => a -> b
inj a
t)
      rws' :: Col N (Row N Z)
rws' = Col i (Row j Z)
Col N (Row N Z)
rws Col N (Row N Z) -> GLT Z -> Col N (Row N Z)
forall {a} {x}.
Embeddable a (ProductForm N (Transformation x)) =>
Col N (Row N x) -> a -> Col N (Row N x)
<* GLT Z
tc
      a :: Z
a    = (Z, N) -> Z
forall a b. (a, b) -> a
fst ((Z, N) -> Z) -> (Z, N) -> Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Row N Z -> (Z, N)
forall j x. Row j x -> (x, j)
rowHead (Row N Z -> (Z, N)) -> Row N Z -> (Z, N)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (Row j Z, i) -> Row N Z
(Row N Z, N) -> Row N Z
forall a b. (a, b) -> a
fst ((Row j Z, i) -> Row N Z) -> (Row j Z, i) -> Row N Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Col i (Row j Z) -> (Row j Z, i)
forall i x. Col i x -> (x, i)
colHead Col i (Row j Z)
rws
      tc :: GLT Z
tc   = Form (GLT Z) -> GLT Z
ProductForm Z (Transformation Z) -> GLT Z
forall x. Constructable x => Form x -> x
make (ProductForm Z (Transformation Z) -> GLT Z)
-> ProductForm Z (Transformation Z) -> GLT Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N
-> Z
-> [(Z, N)]
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
elims N
r Z
a [(Z, i)]
[(Z, N)]
rw (Point (Transformation Z) -> ProductForm Z (Transformation Z)
forall r a. Point a -> ProductForm r a
One Point (Transformation Z)
Dim Z ()
dc) :: GLT Z
      
      elims :: N
-> Z
-> [(Z, N)]
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
elims N
_ Z
_ [] ProductForm Z (Transformation Z)
tc          = ProductForm Z (Transformation Z)
tc
      elims N
r Z
a ((Z
b,N
j):[(Z, N)]
bjs) ProductForm Z (Transformation Z)
tc = N
-> Z
-> [(Z, N)]
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
elims N
r Z
a' [(Z, N)]
bjs (ProductForm Z (Transformation Z)
tc ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm Z (Transformation Z)
tc') where
        (Z
a',ProductForm Z (Transformation Z)
tc') = Dim Z ()
-> (Z, N) -> (Z, N) -> (Z, ProductForm Z (Transformation Z))
forall i.
(i ~ N) =>
Dim Z ()
-> (Z, i) -> (Z, i) -> (Z, ProductForm Z (Transformation Z))
tCols Dim Z ()
dc (Z
a,N
r) (Z
b,N
j)


--------------------------------------------------------------------------------
-- zmxDiagonalForm -

-- | transforming a matrix over Z to a diagonal matrix by applying elements of @'GLT' 'Z'@.
zmxDiagonalForm :: Matrix Z -> DiagonalForm Z
zmxDiagonalForm :: Matrix Z -> DiagonalForm Z
zmxDiagonalForm Matrix Z
m = DiagonalForm Z
m'
  where DiagonalFormStrictPositive DiagonalForm Z
m' = Matrix Z -> DiagonalFormStrictPositive Z
zmxDiagonalFormStrictPositive Matrix Z
m

--------------------------------------------------------------------------------
-- zmxDiagonalFormStrictPositive -

-- | transforming a matrix over Z to a diagonal matrix with strict positive entries
-- by applying elements of @'GLT' 'Z'@.
--
-- __Property__ Let @m@ be in @'Matrix' Z@ and
-- @'DiagonalFormStrictPositive' d = 'zmxDiagonalFormStrictPositive' m@, then holds:
-- @(a 'OAlg.Structure.Operational.*>' m) 'OAlg.Structure.Operational.<*' b '=='
-- 'diagonal' ('rows' m) ('cols' m) ds@ where  @'DiagonalForm' ds a b = d@.
--
-- __Note__ The entries of the diagonal may not be successively divisible, as such
-- it is a pre-form of the Smith Normal Form.
zmxDiagonalFormStrictPositive :: Matrix Z -> DiagonalFormStrictPositive Z
zmxDiagonalFormStrictPositive :: Matrix Z -> DiagonalFormStrictPositive Z
zmxDiagonalFormStrictPositive (Matrix Dim' Z
r Dim' Z
c Entries N N Z
xs)
  = DiagonalForm Z -> DiagonalFormStrictPositive Z
forall k. DiagonalForm k -> DiagonalFormStrictPositive k
DiagonalFormStrictPositive ([Z] -> RowTrafo Z -> ColTrafo Z -> DiagonalForm Z
forall k. [k] -> RowTrafo k -> ColTrafo k -> DiagonalForm k
DiagonalForm [Z]
d (GLT Z -> RowTrafo Z
forall a. GLT a -> RowTrafo a
RowTrafo (GLT Z -> RowTrafo Z) -> GLT Z -> RowTrafo Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Form (GLT Z) -> GLT Z
forall x. Constructable x => Form x -> x
make Form (GLT Z)
ProductForm Z (Transformation Z)
trs) (GLT Z -> ColTrafo Z
forall x. GLT x -> ColTrafo x
ColTrafo (GLT Z -> ColTrafo Z) -> GLT Z -> ColTrafo Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Form (GLT Z) -> GLT Z
forall x. Constructable x => Form x -> x
make Form (GLT Z)
ProductForm Z (Transformation Z)
tcs))
    where ([Z]
d,ProductForm Z (Transformation Z)
trs,ProductForm Z (Transformation Z)
tcs) = Dim Z () -> Dim Z () -> Col N (Row N Z) -> NF Z
forall i j.
(i ~ N, j ~ N) =>
Dim Z () -> Dim Z () -> Col i (Row j Z) -> NF Z
crDiagonalForm Dim Z ()
Dim' Z
r Dim Z ()
Dim' Z
c (Col N (Row N Z) -> NF Z) -> Col N (Row N Z) -> NF Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Entries N N Z -> Col N (Row N Z)
forall i j x. Eq i => Entries i j x -> Col i (Row j x)
etscr Entries N N Z
xs

--------------------------------------------------------------------------------
-- SmithNormalForm -

-- | the smith normal form.
--
-- __Properties__ Let @s = 'SmithNormalForm' o ds a b@ be in @'SmithNormalForm' 'Z'@,
-- then holds: 
--
-- (1) @'snfDiagonalForm' s@ is 'valid'.
--
-- (2) For all @k@ in @ks@ holds: @0 < k@.
--
-- (3) For all @..k':'k'..@ in @ks@ holds: @'mod' k' k '==' 0@.
data SmithNormalForm k = SmithNormalForm N [k] (RowTrafo k) (ColTrafo k)
  deriving (Int -> SmithNormalForm k -> ShowS
[SmithNormalForm k] -> ShowS
SmithNormalForm k -> String
(Int -> SmithNormalForm k -> ShowS)
-> (SmithNormalForm k -> String)
-> ([SmithNormalForm k] -> ShowS)
-> Show (SmithNormalForm k)
forall k. Oriented k => Int -> SmithNormalForm k -> ShowS
forall k. Oriented k => [SmithNormalForm k] -> ShowS
forall k. Oriented k => SmithNormalForm k -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall k. Oriented k => Int -> SmithNormalForm k -> ShowS
showsPrec :: Int -> SmithNormalForm k -> ShowS
$cshow :: forall k. Oriented k => SmithNormalForm k -> String
show :: SmithNormalForm k -> String
$cshowList :: forall k. Oriented k => [SmithNormalForm k] -> ShowS
showList :: [SmithNormalForm k] -> ShowS
Show,SmithNormalForm k -> SmithNormalForm k -> Bool
(SmithNormalForm k -> SmithNormalForm k -> Bool)
-> (SmithNormalForm k -> SmithNormalForm k -> Bool)
-> Eq (SmithNormalForm k)
forall k.
Oriented k =>
SmithNormalForm k -> SmithNormalForm k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall k.
Oriented k =>
SmithNormalForm k -> SmithNormalForm k -> Bool
== :: SmithNormalForm k -> SmithNormalForm k -> Bool
$c/= :: forall k.
Oriented k =>
SmithNormalForm k -> SmithNormalForm k -> Bool
/= :: SmithNormalForm k -> SmithNormalForm k -> Bool
Eq)

--------------------------------------------------------------------------------
-- snfDiagonalForm -

-- | the underlying diagonal form.
snfDiagonalForm :: Semiring k => SmithNormalForm k -> DiagonalForm k
snfDiagonalForm :: forall k. Semiring k => SmithNormalForm k -> DiagonalForm k
snfDiagonalForm (SmithNormalForm N
o [k]
ds RowTrafo k
r ColTrafo k
c)
  = [k] -> RowTrafo k -> ColTrafo k -> DiagonalForm k
forall k. [k] -> RowTrafo k -> ColTrafo k -> DiagonalForm k
DiagonalForm (N -> [k] -> [k]
forall a. N -> [a] -> [a]
takeN N
o (k -> [k]
forall a. a -> [a]
repeat k
forall r. Semiring r => r
rOne) [k] -> [k] -> [k]
forall a. [a] -> [a] -> [a]
++ [k]
ds) RowTrafo k
r ColTrafo k
c

--------------------------------------------------------------------------------
-- SmithNormalForm - Validable -

instance Validable (SmithNormalForm Z) where
  valid :: SmithNormalForm Z -> Statement
valid s :: SmithNormalForm Z
s@(SmithNormalForm N
_ [Z]
ks RowTrafo Z
_ ColTrafo Z
_) = String -> Label
Label String
"SmithNormalForm" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ DiagonalForm Z -> Statement
forall a. Validable a => a -> Statement
valid (SmithNormalForm Z -> DiagonalForm Z
forall k. Semiring k => SmithNormalForm k -> DiagonalForm k
snfDiagonalForm SmithNormalForm Z
s)
        , N -> [Z] -> Statement
forall {a} {t}.
(Num a, Integral a, Enum t, Show t) =>
t -> [a] -> Statement
vld (N
0::N) [Z]
ks
        ] where

    vld0 :: b -> a -> Statement
vld0 b
i a
k = String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
k)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"(k,i)"String -> String -> Parameter
:=(a, b) -> String
forall a. Show a => a -> String
show (a
k,b
i)]
    
    vld :: t -> [a] -> Statement
vld t
_ []  = Statement
SValid
    vld t
i [a
k] = t -> a -> Statement
forall {a} {b}.
(Ord a, Num a, Show a, Show b) =>
b -> a -> Statement
vld0 t
i a
k
    vld t
i (a
k:a
k':[a]
ks)
      = [Statement] -> Statement
And [ t -> a -> Statement
forall {a} {b}.
(Ord a, Num a, Show a, Show b) =>
b -> a -> Statement
vld0 t
i a
k
            , String -> Label
Label String
"3" Label -> Statement -> Statement
:<=>: (a
k' a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
k a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0)
                Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"i"String -> String -> Parameter
:=t -> String
forall a. Show a => a -> String
show t
i,String
"(k,k')"String -> String -> Parameter
:=(a, a) -> String
forall a. Show a => a -> String
show (a
k,a
k')]

            , t -> [a] -> Statement
vld (t -> t
forall a. Enum a => a -> a
succ t
i) (a
k'a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ks)
            ]

instance Entity (SmithNormalForm Z)

--------------------------------------------------------------------------------
-- smithNormalForm -

-- | Smith Normal Form of a matrix.
--
-- __Property__ Let @m@ be in @'Matrix' 'Z'@ and
-- @'SmithNormalForm o ds a b = 'smithNormalForm' m@, then holds:
-- @(a 'OAlg.Structure.Operational.*>' m) 'OAlg.Structure.Operational.<*' b '=='
-- 'diagonal' ('rows' m) ('cols' m) ds@ where
-- @ds = ('takeN' o '$' 'repeat' 1) '++' ds'@. 
smithNormalForm :: Matrix Z -> SmithNormalForm Z
smithNormalForm :: Matrix Z -> SmithNormalForm Z
smithNormalForm = DiagonalFormStrictPositive Z -> SmithNormalForm Z
smithNormalForm' (DiagonalFormStrictPositive Z -> SmithNormalForm Z)
-> (Matrix Z -> DiagonalFormStrictPositive Z)
-> Matrix Z
-> SmithNormalForm Z
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
. Matrix Z -> DiagonalFormStrictPositive Z
zmxDiagonalFormStrictPositive

  
-- | Smith Normal Form of a diagonal matrix over 'Z' with strict positive entries.
--
-- __Property__ Let @d = 'DiagonalFormStrictPositive' d' ('DiagonalForm' ds a b)@ be in
-- @'DiagonalFormStrictPositive' 'Z'@, @m = 'dgfMatrix' d'@ and
-- @s = 'smithNormalForm'' d@, then holds: @m '==' 'dgfMatrix' ('snfDiagonalForm' s)@.
smithNormalForm' :: DiagonalFormStrictPositive Z -> SmithNormalForm Z
smithNormalForm' :: DiagonalFormStrictPositive Z -> SmithNormalForm Z
smithNormalForm' (DiagonalFormStrictPositive (DiagonalForm [Z]
ds (RowTrafo GLT Z
a) (ColTrafo GLT Z
b)))
  = N -> [Z] -> RowTrafo Z -> ColTrafo Z -> SmithNormalForm Z
forall k. N -> [k] -> RowTrafo k -> ColTrafo k -> SmithNormalForm k
SmithNormalForm N
o [Z]
ds'' (GLT Z -> RowTrafo Z
forall a. GLT a -> RowTrafo a
RowTrafo (GLT Z -> RowTrafo Z) -> GLT Z -> RowTrafo Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Form (GLT Z) -> GLT Z
forall x. Constructable x => Form x -> x
make (ProductForm Z (Transformation Z)
a'ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*GLT Z -> Form (GLT Z)
forall x. Exposable x => x -> Form x
form GLT Z
a)) (GLT Z -> ColTrafo Z
forall x. GLT x -> ColTrafo x
ColTrafo (GLT Z -> ColTrafo Z) -> GLT Z -> ColTrafo Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Form (GLT Z) -> GLT Z
forall x. Constructable x => Form x -> x
make (GLT Z -> Form (GLT Z)
forall x. Exposable x => x -> Form x
form GLT Z
bProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*ProductForm Z (Transformation Z)
b'))
  where
  ([Z]
ds',ProductForm Z (Transformation Z)
a',ProductForm Z (Transformation Z)
b') = (NF Z -> Rdc (NF Z)) -> NF Z -> NF Z
forall x. (x -> Rdc x) -> x -> x
reduceWith (Dim' Z -> Dim' Z -> NF Z -> Rdc (NF Z)
dnf4 Point (GLT Z)
Dim' Z
n Point (GLT Z)
Dim' Z
m) ([Z]
ds,Point (Transformation Z) -> ProductForm Z (Transformation Z)
forall r a. Point a -> ProductForm r a
One Point (GLT Z)
Point (Transformation Z)
n,Point (Transformation Z) -> ProductForm Z (Transformation Z)
forall r a. Point a -> ProductForm r a
One Point (GLT Z)
Point (Transformation Z)
m)
  n :: Point (GLT Z)
n = GLT Z -> Point (GLT Z)
forall q. Oriented q => q -> Point q
start GLT Z
a
  m :: Point (GLT Z)
m = GLT Z -> Point (GLT Z)
forall q. Oriented q => q -> Point q
end GLT Z
b
  ds'' :: [Z]
ds'' = (Z -> Bool) -> [Z] -> [Z]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Z -> Z -> Bool
forall a. Eq a => a -> a -> Bool
==Z
1) [Z]
ds'
  o :: N
o = [Z] -> N
forall x. LengthN x => x -> N
lengthN [Z]
ds' N -> N -> N
>- [Z] -> N
forall x. LengthN x => x -> N
lengthN [Z]
ds''

-- | reduces the diagonal entries @...d':'d'... = ds@ to smith normal form entries,
--   i.e. @d' `mod` d '==' 0@.
dnf4 :: Dim' Z -> Dim' Z -> NF Z -> Rdc (NF Z )
dnf4 :: Dim' Z -> Dim' Z -> NF Z -> Rdc (NF Z)
dnf4 Dim' Z
n Dim' Z
m = NF Z -> Rdc (NF Z)
rdcSort (NF Z -> Rdc (NF Z)) -> (NF Z -> Rdc (NF Z)) -> NF Z -> Rdc (NF Z)
forall x. (x -> Rdc x) -> (x -> Rdc x) -> x -> Rdc x
>>>= N -> NF Z -> Rdc (NF Z)
rdcDiv (N
0::N) where
  
  rdcSort :: NF Z -> Rdc (NF Z)
rdcSort d :: NF Z
d@([Z]
ds,ProductForm Z (Transformation Z)
a,ProductForm Z (Transformation Z)
b) = if Permutation N
p Permutation N -> Permutation N -> Bool
forall a. Eq a => a -> a -> Bool
== Point (Permutation N) -> Permutation N
forall c. Multiplicative c => Point c -> c
one ()
    then NF Z -> Rdc (NF Z)
forall a. a -> Action RdcState a
forall (m :: * -> *) a. Monad m => a -> m a
return NF Z
d
    else NF Z -> Rdc (NF Z)
forall a. a -> Action RdcState a
reducesTo ([Z]
ds',Transformation Z -> ProductForm Z (Transformation Z)
forall r a. a -> ProductForm r a
P (Dim' Z -> Dim' Z -> Permutation N -> Transformation Z
forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim' Z
n Dim' Z
n Permutation N
p)ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*ProductForm Z (Transformation Z)
a,ProductForm Z (Transformation Z)
bProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*Transformation Z -> ProductForm Z (Transformation Z)
forall r a. a -> ProductForm r a
P(Dim' Z -> Dim' Z -> Permutation N -> Transformation Z
forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim' Z
m Dim' Z
m (Permutation N -> Permutation N
forall c. Invertible c => c -> c
invert Permutation N
p)))
    where ([Z]
ds',Permutation N
p) = (Z -> Z -> Ordering) -> (Z -> Z) -> [Z] -> ([Z], Permutation N)
forall (s :: * -> *) x w.
PermutableSequence s N x =>
(w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation N)
permuteByN Z -> Z -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Z -> Z
forall x. x -> x
id [Z]
ds

  rdcDiv :: N -> NF Z -> Rdc (NF Z)
rdcDiv N
i ([Z]
ds,ProductForm Z (Transformation Z)
a,ProductForm Z (Transformation Z)
b) = case [Z]
ds of
    (Z
d:Z
d':[Z]
ds') | Z
d' Z -> Z -> Z
forall a. Integral a => a -> a -> a
`mod` Z
d Z -> Z -> Bool
forall a. Eq a => a -> a -> Bool
/= Z
0
      -> NF Z -> Rdc (NF Z)
forall a. a -> Action RdcState a
reducesTo (Z
eZ -> [Z] -> [Z]
forall a. a -> [a] -> [a]
:Z
e'Z -> [Z] -> [Z]
forall a. a -> [a] -> [a]
:[Z]
ds',ProductForm Z (Transformation Z)
a'ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*ProductForm Z (Transformation Z)
a,ProductForm Z (Transformation Z)
bProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*Transformation Z -> ProductForm Z (Transformation Z)
forall r a. a -> ProductForm r a
P (Dim' Z -> N -> N -> GL2 Z -> Transformation Z
forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim' Z
m N
i N
i' (Z -> Z -> Z -> Z -> GL2 Z
forall x. x -> x -> x -> x -> GL2 x
GL2 Z
1 Z
0 Z
1 Z
1))ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
-> ProductForm Z (Transformation Z)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*ProductForm Z (Transformation Z)
b') where
          i' :: N
i' = N -> N
forall a. Enum a => a -> a
succ N
i
          ([Z
e,Z
e'],ProductForm Z (Transformation Z)
a',ProductForm Z (Transformation Z)
b') = N -> Dim' Z -> Dim' Z -> Col N (Row N Z) -> NF Z
forall i j.
(i ~ N, j ~ N) =>
i -> Dim' Z -> Dim' Z -> Col i (Row j Z) -> NF Z
dnf' N
i Dim' Z
n Dim' Z
m (Entries N N Z -> Col N (Row N Z)
forall i j x. Eq i => Entries i j x -> Col i (Row j x)
etscr Entries N N Z
xs)
          -- from ds is stirct positive follows that dnf yields a diagonal with two elements 
          xs :: Entries N N Z
xs = PSequence (N, N) Z -> Entries N N Z
forall i j x. PSequence (i, j) x -> Entries i j x
Entries (PSequence (N, N) Z -> Entries N N Z)
-> PSequence (N, N) Z -> Entries N N Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(Z, (N, N))] -> PSequence (N, N) Z
forall i x. [(x, i)] -> PSequence i x
PSequence [(Z
d,(N
i,N
i)),(Z
d',(N
i',N
i)),(Z
d',(N
i',N
i'))] 
                   
    (Z
d:[Z]
ds') -> N -> NF Z -> Rdc (NF Z)
rdcDiv (N -> N
forall a. Enum a => a -> a
succ N
i) ([Z]
ds',ProductForm Z (Transformation Z)
a,ProductForm Z (Transformation Z)
b) Rdc (NF Z) -> (NF Z -> Rdc (NF Z)) -> Rdc (NF Z)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \([Z]
ds',ProductForm Z (Transformation Z)
a,ProductForm Z (Transformation Z)
b) -> NF Z -> Rdc (NF Z)
forall a. a -> Action RdcState a
forall (m :: * -> *) a. Monad m => a -> m a
return (Z
dZ -> [Z] -> [Z]
forall a. a -> [a] -> [a]
:[Z]
ds',ProductForm Z (Transformation Z)
a,ProductForm Z (Transformation Z)
b)
    
    [Z]
_       -> NF Z -> Rdc (NF Z)
forall a. a -> Action RdcState a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Z]
ds,ProductForm Z (Transformation Z)
a,ProductForm Z (Transformation Z)
b)

--------------------------------------------------------------------------------
-- prpDiagonalFormZ -

-- | validating diagonal and Smith Normal form for 'Z'-matrices.
prpDiagonalFormZ :: N -> Q -> Statement
prpDiagonalFormZ :: N -> Q -> Statement
prpDiagonalFormZ N
dMax Q
dens = String -> Label
Prp String
"DiagonalFormZ" Label -> Statement -> Statement
:<=>:
  X (Matrix Z) -> (Matrix Z -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (XOrtOrientation (Matrix Z) -> X (Matrix Z)
forall q. XOrtOrientation q -> XOrt q
xoOrt (XOrtOrientation (Matrix Z) -> X (Matrix Z))
-> XOrtOrientation (Matrix Z) -> X (Matrix Z)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> Q -> X Z -> XOrtOrientation (Matrix Z)
forall x.
(Distributive x, Total x) =>
N -> Q -> X x -> XOrtOrientation (Matrix x)
xMatrixTtl N
dMax Q
dens X Z
forall x. XStandard x => X x
xStandard)
    (\Matrix Z
m -> let d :: DiagonalFormStrictPositive Z
d@(DiagonalFormStrictPositive DiagonalForm Z
d') = Matrix Z -> DiagonalFormStrictPositive Z
zmxDiagonalFormStrictPositive Matrix Z
m
               s :: SmithNormalForm Z
s = DiagonalFormStrictPositive Z -> SmithNormalForm Z
smithNormalForm' DiagonalFormStrictPositive Z
d
           in
             [Statement] -> Statement
And [ (DiagonalFormStrictPositive Z, SmithNormalForm Z) -> Statement
forall a. Validable a => a -> Statement
valid (DiagonalFormStrictPositive Z
d,SmithNormalForm Z
s)
                 , String -> Label
Label String
"DiagonalForm" Label -> Statement -> Statement
:<=>:
                     (Matrix Z
m Matrix Z -> Matrix Z -> Bool
forall a. Eq a => a -> a -> Bool
== DiagonalForm Z -> Matrix Z
forall k. Distributive k => DiagonalForm k -> Matrix k
dgfMatrix DiagonalForm Z
d')Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"m"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
m]
                 , String -> Label
Label String
"SmithNormalForm" Label -> Statement -> Statement
:<=>:
                     (Matrix Z
m Matrix Z -> Matrix Z -> Bool
forall a. Eq a => a -> a -> Bool
== DiagonalForm Z -> Matrix Z
forall k. Distributive k => DiagonalForm k -> Matrix k
dgfMatrix (SmithNormalForm Z -> DiagonalForm Z
forall k. Semiring k => SmithNormalForm k -> DiagonalForm k
snfDiagonalForm SmithNormalForm Z
s))Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"m"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
m]
                 ]
    )