{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE
    TypeFamilies
  , FlexibleInstances
  , GADTs
  , MultiParamTypeClasses
  , StandaloneDeriving
#-}

-- |
-- Module      : OAlg.Entity.Matrix.Vector
-- Description : vectors with coefficients lying in a semi rings.
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- 'Vector's with coefficients, lying in a 'Semiring'.
module OAlg.Entity.Matrix.Vector
  ( -- * Vector
    Vector(..), vecpsq, cf, cfsssy, ssycfs, vecrc, vecAppl

    -- * Hom
  , HomSymbol(..), mtxHomSymbol
  
    -- * Representation
  , repMatrix, Representable(..), mtxRepresentable

    -- * Propostion
  , prpRepMatrix, prpRepMatrixZ

    -- * X
  , xVecN
  ) where

import Control.Monad

import Data.Typeable

import Data.List (map,(++))
import Data.Foldable

import OAlg.Prelude

import OAlg.Data.Singleton
-- import OAlg.Data.Ord

import OAlg.Structure.Fibred
import OAlg.Structure.Additive
import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Ring
import OAlg.Structure.Exponential
import OAlg.Structure.Vectorial

import OAlg.Entity.Sequence hiding (sy)
import OAlg.Entity.Sum

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

import OAlg.Hom.Definition
import OAlg.Hom.Fibred
import OAlg.Hom.Additive
import OAlg.Hom.Vectorial

--------------------------------------------------------------------------------
-- Vector -

-- | vector with coefficients lying in a 'Semiring', indexd by 'N'.
--
-- __Definition__ Let @v = 'Vector' ris@ be in @'Vector' __r__@ with @__r__@ be a 'Semiring',
-- then @v@ is 'valid' iff
--
-- (1) @ris@ is 'valid'
--
-- (2) For all @(r,i)@ in @ris@ holds: @r@ is not equal to 'rZero'.
newtype Vector r = Vector (PSequence N r) deriving (Int -> Vector r -> ShowS
forall r. Show r => Int -> Vector r -> ShowS
forall r. Show r => [Vector r] -> ShowS
forall r. Show r => Vector r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Vector r] -> ShowS
$cshowList :: forall r. Show r => [Vector r] -> ShowS
show :: Vector r -> String
$cshow :: forall r. Show r => Vector r -> String
showsPrec :: Int -> Vector r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> Vector r -> ShowS
Show,Vector r -> Vector r -> Bool
forall r. Eq r => Vector r -> Vector r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Vector r -> Vector r -> Bool
$c/= :: forall r. Eq r => Vector r -> Vector r -> Bool
== :: Vector r -> Vector r -> Bool
$c== :: forall r. Eq r => Vector r -> Vector r -> Bool
Eq,Vector r -> Vector r -> Bool
Vector r -> Vector r -> Ordering
Vector r -> Vector r -> Vector r
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {r}. Ord r => Eq (Vector r)
forall r. Ord r => Vector r -> Vector r -> Bool
forall r. Ord r => Vector r -> Vector r -> Ordering
forall r. Ord r => Vector r -> Vector r -> Vector r
min :: Vector r -> Vector r -> Vector r
$cmin :: forall r. Ord r => Vector r -> Vector r -> Vector r
max :: Vector r -> Vector r -> Vector r
$cmax :: forall r. Ord r => Vector r -> Vector r -> Vector r
>= :: Vector r -> Vector r -> Bool
$c>= :: forall r. Ord r => Vector r -> Vector r -> Bool
> :: Vector r -> Vector r -> Bool
$c> :: forall r. Ord r => Vector r -> Vector r -> Bool
<= :: Vector r -> Vector r -> Bool
$c<= :: forall r. Ord r => Vector r -> Vector r -> Bool
< :: Vector r -> Vector r -> Bool
$c< :: forall r. Ord r => Vector r -> Vector r -> Bool
compare :: Vector r -> Vector r -> Ordering
$ccompare :: forall r. Ord r => Vector r -> Vector r -> Ordering
Ord)

--------------------------------------------------------------------------------
-- vecpsq -

-- | the underlying partial sequence.
vecpsq :: Vector r -> PSequence N r
vecpsq :: forall r. Vector r -> PSequence N r
vecpsq (Vector PSequence N r
ris) = PSequence N r
ris

--------------------------------------------------------------------------------
-- vector -

-- | the induced vector.
vector :: Semiring r => [(r,N)] -> Vector r
vector :: forall r. Semiring r => [(r, N)] -> Vector r
vector = forall r. PSequence N r -> Vector r
Vector forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (forall b. Boolean b => b -> b
not forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Additive a => a -> Bool
isZero) forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall i x. Ord i => (x -> x -> x) -> [(x, i)] -> PSequence i x
psequence forall a. Additive a => a -> a -> a
(+)

--------------------------------------------------------------------------------
-- cf -

-- | the @i@-th coefficient of the given vector.
--
-- __Example__ Let @v = 'vector' [(-3,2),(9,4)] :: 'Vector' 'Z'@
--
-- >>> map (cf v) [0..8]
-- [0,0,-3,0,9,0,0,0,0]
cf :: Semiring r => Vector r -> N -> r
cf :: forall r. Semiring r => Vector r -> N -> r
cf (Vector PSequence N r
v) N
i = forall a. a -> Maybe a -> a
fromMaybe forall r. Semiring r => r
rZero (PSequence N r
v forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
?? N
i)

--------------------------------------------------------------------------------
-- Vector - Entity -

instance Semiring r => Validable (Vector r) where
  valid :: Vector r -> Statement
valid v :: Vector r
v@(Vector PSequence N r
ris) = (String -> Label
Label forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Show a => a -> String
show forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Typeable a => a -> TypeRep
typeOf Vector r
v) Label -> Statement -> Statement
:<=>: forall {b} {a}.
(Ord b, Additive a, Entity b) =>
PSequence b a -> Statement
vldVec PSequence N r
ris where
    vldVec :: PSequence b a -> Statement
vldVec PSequence b a
ris
      = [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid PSequence b a
ris
            , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall {a} {b}.
(Additive a, Show b) =>
Statement -> (a, b) -> Statement
vldxs Statement
SValid (forall i x. PSequence i x -> [(x, i)]
psqxs PSequence b a
ris)
            ]

    vldxs :: Statement -> (a, b) -> Statement
vldxs Statement
s (a, b)
ri
      = [Statement] -> Statement
And [ Statement
s
            , (forall b. Boolean b => b -> b
not forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Additive a => a -> Bool
isZero forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a, b) -> a
fst (a, b)
ri) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(r,i)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (a, b)
ri]
            ]

instance Semiring r => Entity (Vector r)

--------------------------------------------------------------------------------
-- Vector - Euclidean -

instance Semiring r => Fibred (Vector r) where
  type Root (Vector r) = ()
  root :: Vector r -> Root (Vector r)
root Vector r
_ = ()

instance Semiring r => Additive (Vector r) where
  zero :: Root (Vector r) -> Vector r
zero Root (Vector r)
_ = forall r. PSequence N r -> Vector r
Vector forall i x. PSequence i x
psqEmpty
  
  Vector PSequence N r
v + :: Vector r -> Vector r -> Vector r
+ Vector PSequence N r
w = forall r. PSequence N r -> Vector r
Vector (forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (forall b. Boolean b => b -> b
not forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Additive a => a -> Bool
isZero) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x y z.
Ord i =>
(x -> y -> z)
-> (x -> z)
-> (y -> z)
-> PSequence i x
-> PSequence i y
-> PSequence i z
psqInterlace forall a. Additive a => a -> a -> a
(+) forall x. x -> x
id forall x. x -> x
id PSequence N r
v PSequence N r
w)
    
  ntimes :: N -> Vector r -> Vector r
ntimes N
x (Vector PSequence N r
v) = forall r. PSequence N r -> Vector r
Vector (forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (forall b. Boolean b => b -> b
not forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Additive a => a -> Bool
isZero) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap (forall a. Additive a => N -> a -> a
ntimes N
x) PSequence N r
v)

instance Ring r => Abelian (Vector r) where
  negate :: Vector r -> Vector r
negate (Vector PSequence N r
v) = forall r. PSequence N r -> Vector r
Vector (forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap forall a. Abelian a => a -> a
negate PSequence N r
v)
  ztimes :: Z -> Vector r -> Vector r
ztimes Z
x (Vector PSequence N r
v) = forall r. PSequence N r -> Vector r
Vector (forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (forall b. Boolean b => b -> b
not forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Additive a => a -> Bool
isZero) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap (forall a. Abelian a => Z -> a -> a
ztimes Z
x) PSequence N r
v)

instance (Semiring r, Commutative r) => Vectorial (Vector r) where
  type Scalar (Vector r) = r
  Scalar (Vector r)
r ! :: Scalar (Vector r) -> Vector r -> Vector r
! (Vector PSequence N r
v) = forall r. PSequence N r -> Vector r
Vector (forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (forall b. Boolean b => b -> b
not forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Additive a => a -> Bool
isZero) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap (Scalar (Vector r)
rforall c. Multiplicative c => c -> c -> c
*) PSequence N r
v)

instance (Semiring r, Commutative r) => Euclidean (Vector r) where
  Vector PSequence N r
v <!> :: Vector r -> Vector r -> Scalar (Vector r)
<!> Vector PSequence N r
w
    = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Additive a => a -> a -> a
(+) forall r. Semiring r => r
rZero
    forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst
    forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. PSequence i x -> [(x, i)]
psqxs
    forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x y z.
Ord i =>
(x -> y -> z)
-> (x -> z)
-> (y -> z)
-> PSequence i x
-> PSequence i y
-> PSequence i z
psqInterlace forall c. Multiplicative c => c -> c -> c
(*) (forall b a. b -> a -> b
const forall r. Semiring r => r
rZero) (forall b a. b -> a -> b
const forall r. Semiring r => r
rZero) PSequence N r
v PSequence N r
w

--------------------------------------------------------------------------------
-- ssycfs -

-- | the associated coefficients of a free sum of symbols according to the given set of symbols.
--
-- __Property__ Let @s = s 0 '<' s 1 '<' ..@ be in @'Set' __a__@ and @x@ in
-- @'SumSymbol' __r__ __a__@ then holds:
-- @'ssyprj' s x '==' 'cf' r 0 '!' 'sy' (s 0) '+' 'cf' r  1 '!' 'sy' (s 1) '+' ..@ where
-- @r = 'ssycfs' s x@, 
ssycfs :: (Semiring r, Ord a) => Set a -> SumSymbol r a -> Vector r
ssycfs :: forall r a.
(Semiring r, Ord a) =>
Set a -> SumSymbol r a -> Vector r
ssycfs Set a
s SumSymbol r a
x = forall r. PSequence N r -> Vector r
Vector (forall i j x.
(Ord i, Ord j) =>
PSequence i x -> PSequence j i -> PSequence j x
psqCompose (forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. LinearCombination r a -> [(r, a)]
lcs forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. Semiring r => SumSymbol r a -> LinearCombination r a
ssylc SumSymbol r a
x) (forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN Set a
s))
                              -- :: PSequence a r            :: PSequence N a
             
--------------------------------------------------------------------------------
-- cfsssy -

-- | the associated free sum of symbols according to the given set of symbols and coefficients.
--
-- __Property__ Let @s = s 0 '<' s 1 '<' ..@ be in @'Set' __a__@ and
-- @r@ be in @'Vector' __r__@ then holds:
-- @'cfsssy' s r '==' 'cf' r 0 '!' 'sy' (s 0) '+' 'cf' r  1 '!' 'sy' (s 1) '+' ..@.
cfsssy :: (Semiring r, Commutative r, Entity a, Ord a) => Set a -> Vector r -> SumSymbol r a
cfsssy :: forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
Set a -> Vector r -> SumSymbol r a
cfsssy Set a
s Vector r
v = forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
[(r, a)] -> SumSymbol r a
sumSymbol forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. PSequence i x -> [(x, i)]
psqxs forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i j x.
(Ord i, Ord j) =>
PSequence i x -> PSequence j i -> PSequence j x
psqCompose (forall r. Vector r -> PSequence N r
vecpsq Vector r
v) (forall i x. [(x, i)] -> PSequence i x
PSequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(a
a,N
i) -> (N
i,a
a)) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN Set a
s)
                             -- :: PSequence i r    :: PSeqeunce a i
                             -- :: PSequence a r

--------------------------------------------------------------------------------
-- vecrc -

-- | a vector as a row with one column at @0@.
vecrc :: Vector r -> Row N (Col N r)
vecrc :: forall r. Vector r -> Row N (Col N r)
vecrc (Vector (PSequence []))  = forall j x. Row j x
rowEmpty
vecrc (Vector PSequence N r
v)               = forall j x. PSequence j x -> Row j x
Row forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. [(x, i)] -> PSequence i x
PSequence [(forall i x. PSequence i x -> Col i x
Col PSequence N r
v,N
0)]

--------------------------------------------------------------------------------
-- vecAppl -

-- | applying a matrix from the left.
vecAppl :: Semiring r => Matrix r -> Vector r -> Vector r
vecAppl :: forall r. Semiring r => Matrix r -> Vector r -> Vector r
vecAppl Matrix r
m Vector r
v = forall r. Col N (Row N r) -> Vector r
crvec (forall x. Matrix x -> Col N (Row N x)
mtxColRow Matrix r
m forall x k i j.
(Distributive x, Ord k) =>
Col i (Row k x) -> Row j (Col k x) -> Col i (Row j x)
`etsMlt` forall r. Vector r -> Row N (Col N r)
vecrc Vector r
v) where

    crvec :: Col N (Row N r) -> Vector r
    crvec :: forall r. Col N (Row N r) -> Vector r
crvec Col N (Row N r)
cl = case forall j i a. Eq j => j -> Col i (Row j a) -> Col i a
crHeadColAt N
0 Col N (Row N r)
cl of Col PSequence N r
v -> forall r. PSequence N r -> Vector r
Vector PSequence N r
v

--------------------------------------------------------------------------------
-- HomSymbol -

data HomSymbol r x y where
  HomSymbol :: (Entity x, Ord x, Entity y, Ord y)
    => PSequence x (LinearCombination r y) -> HomSymbol r (SumSymbol r x) (SumSymbol r y)
  Cfs :: (Entity x, Ord x) => Set x -> HomSymbol r (SumSymbol r x) (Vector r)
  Ssy :: (Entity x, Ord x) => Set x -> HomSymbol r (Vector r) (SumSymbol r x)
  HomMatrix :: Matrix r -> HomSymbol r (Vector r) (Vector r)

--------------------------------------------------------------------------------
-- HomSymbol - Entity -

deriving instance Semiring r => Show (HomSymbol r x y)
instance Semiring r => Show2 (HomSymbol r) 

deriving instance Semiring r => Eq (HomSymbol r x y)
instance Semiring r => Eq2 (HomSymbol r)

instance Semiring r => Validable (HomSymbol r x y) where
  valid :: HomSymbol r x y -> Statement
valid HomSymbol r x y
h = case HomSymbol r x y
h of
    HomSymbol PSequence x (LinearCombination r y)
lcs -> String -> Label
Label String
"HomSymbol" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid PSequence x (LinearCombination r y)
lcs
    Cfs Set x
xs        -> String -> Label
Label String
"Cfs" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid Set x
xs
    Ssy Set x
xs        -> String -> Label
Label String
"Ssy" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid Set x
xs
    HomMatrix Matrix r
m   -> String -> Label
Label String
"HomMatrix" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid Matrix r
m
instance Semiring r => Validable2 (HomSymbol r)

instance (Semiring r, Typeable x, Typeable y) => Entity (HomSymbol r x y)
instance Semiring r => Entity2 (HomSymbol r)

--------------------------------------------------------------------------------
-- HomSymbol - HomVectorial -

instance (Semiring r, Commutative r) => Applicative (HomSymbol r) where
  amap :: forall a b. HomSymbol r a b -> a -> b
amap (HomSymbol PSequence x (LinearCombination r y)
lcs) a
s = forall r y x.
(Semiring r, Commutative r, Entity y, Ord y) =>
(x -> LinearCombination r y) -> SumSymbol r x -> SumSymbol r y
ssySum x -> LinearCombination r y
f a
s where
    f :: x -> LinearCombination r y
f x
x = case PSequence x (LinearCombination r y)
lcs forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
?? x
x of
      Just LinearCombination r y
lc -> LinearCombination r y
lc
      Maybe (LinearCombination r y)
Nothing -> forall r a. [(r, a)] -> LinearCombination r a
LinearCombination []
  amap (Cfs Set x
xs) a
s = forall r a.
(Semiring r, Ord a) =>
Set a -> SumSymbol r a -> Vector r
ssycfs Set x
xs a
s
  amap (Ssy Set x
xs) a
v = forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
Set a -> Vector r -> SumSymbol r a
cfsssy Set x
xs a
v
  amap (HomMatrix Matrix r
m) a
v = forall r. Semiring r => Matrix r -> Vector r -> Vector r
vecAppl Matrix r
m a
v

instance (Semiring r, Commutative r) => Morphism (HomSymbol r) where
  type ObjectClass (HomSymbol r) = Vec r
  homomorphous :: forall x y.
HomSymbol r x y -> Homomorphous (ObjectClass (HomSymbol r)) x y
homomorphous HomSymbol r x y
m = case HomSymbol r x y
m of
    HomSymbol PSequence x (LinearCombination r y)
_ -> forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
    Cfs Set x
_       -> forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
    Ssy Set x
_       -> forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
    HomMatrix Matrix r
_ -> forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  

instance (Semiring r, Commutative r) => EmbeddableMorphism (HomSymbol r) Fbr
instance (Semiring r, Commutative r) => EmbeddableMorphism (HomSymbol r) Typ
instance (Semiring r, Commutative r) => EmbeddableMorphismTyp (HomSymbol r) 
instance (Semiring r, Commutative r) => HomFibred (HomSymbol r) where
  rmap :: forall a b. HomSymbol r a b -> Root a -> Root b
rmap (HomSymbol PSequence x (LinearCombination r y)
_) = forall b a. b -> a -> b
const ()
  rmap (Cfs Set x
_)       = forall b a. b -> a -> b
const ()
  rmap (Ssy Set x
_)       = forall b a. b -> a -> b
const ()
  rmap (HomMatrix Matrix r
_) = forall b a. b -> a -> b
const ()

instance (Semiring r, Commutative r) => EmbeddableMorphism (HomSymbol r) Add
instance (Semiring r, Commutative r) => HomAdditive (HomSymbol r)

instance (Semiring r, Commutative r) => EmbeddableMorphism (HomSymbol r) (Vec r)
instance (Semiring r, Commutative r) => HomVectorial r (HomSymbol r)

--------------------------------------------------------------------------------
-- Representable -

-- | Predicate for a @__r__@-linear homomorphisms between the free sums @'SumSymbol' __r__ __x__@
-- and @'SumSymbol' __r__ __y__@ being /representable/ for the given symbol sets.
--
-- __Definition__ Let @l@ be in @'LinearCombination' __r__ __x__@ and @xs@ be a 'Set' of symbols of
-- @__x__@, then @l@ is called __/representable in/__ @xs@ iff all symbols of @'lcs' l@ are elements
-- of @xs@.
--
-- __Property__ Let @h@ be a @__r__@-linear homomorphism between the free sums
-- @'SumSymbol' __r__ __x__@ and @'SumSymbol' __r__ __y__@, @xs@ a 'Set' of symbols in @__x__@ and
-- @ys@ a 'Set' of symbols in @__y__@, then holds: If for each symbol @x@ in @xs@ the associated
-- 'LinearCombination' of @h '$' x@ is representable in @ys@, then @'Representable' h xs ys@ is
-- 'valid'.
data Representable r h x y where
  Representable :: (Hom (Vec r) h, Entity x, Ord x, Entity y, Ord y)
    => h (SumSymbol r x) (SumSymbol r y) -> Set x -> Set y
    -> Representable r h (SumSymbol r x) (SumSymbol r y)

instance Show (Representable r h x y) where
  show :: Representable r h x y -> String
show (Representable h (SumSymbol r x) (SumSymbol r y)
h Set x
xs Set y
ys)
    = String
"Representable " forall a. [a] -> [a] -> [a]
++ forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h (SumSymbol r x) (SumSymbol r y)
h forall a. [a] -> [a] -> [a]
++ String
" (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set x
xs forall a. [a] -> [a] -> [a]
++ String
") (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set y
ys forall a. [a] -> [a] -> [a]
++ String
")"

instance Validable (Representable r h x y) where
  valid :: Representable r h x y -> Statement
valid (Representable h (SumSymbol r x) (SumSymbol r y)
h Set x
xs Set y
ys) = String -> Label
Label String
"Representable"
    Label -> Statement -> Statement
:<=>: forall r (h :: * -> * -> *) x y.
(Hom (Vec r) h, Entity x, Ord x, Ord y) =>
Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
-> h (SumSymbol r x) (SumSymbol r y) -> Set x -> Set y -> Statement
vldsVec (forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h (SumSymbol r x) (SumSymbol r y)
h)) h (SumSymbol r x) (SumSymbol r y)
h Set x
xs Set y
ys where

    vldsVec :: (Hom (Vec r) h, Entity x, Ord x, Ord y)
      => Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
      -> h (SumSymbol r x) (SumSymbol r y) -> Set x -> Set y -> Statement
    vldsVec :: forall r (h :: * -> * -> *) x y.
(Hom (Vec r) h, Entity x, Ord x, Ord y) =>
Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
-> h (SumSymbol r x) (SumSymbol r y) -> Set x -> Set y -> Statement
vldsVec (Struct (Vec r) (SumSymbol r x)
Struct :>: Struct (Vec r) (SumSymbol r y)
_) h (SumSymbol r x) (SumSymbol r y)
h Set x
xs Set y
ys = forall r (h :: * -> * -> *) x y.
(Semiring r, Commutative r, Hom (Vec r) h, Entity x, Ord x,
 Ord y) =>
h (SumSymbol r x) (SumSymbol r y) -> [(x, N)] -> Set y -> Statement
vlds h (SumSymbol r x) (SumSymbol r y)
h (forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN Set x
xs) Set y
ys

    vlds :: (Semiring r, Commutative r, Hom (Vec r) h, Entity x, Ord x, Ord y)
      => h (SumSymbol r x) (SumSymbol r y) -> [(x,N)] -> Set y -> Statement
    vlds :: forall r (h :: * -> * -> *) x y.
(Semiring r, Commutative r, Hom (Vec r) h, Entity x, Ord x,
 Ord y) =>
h (SumSymbol r x) (SumSymbol r y) -> [(x, N)] -> Set y -> Statement
vlds h (SumSymbol r x) (SumSymbol r y)
_ [] Set y
_           = Statement
SValid
    vlds h (SumSymbol r x) (SumSymbol r y)
h ((x
x,N
j):[(x, N)]
xjs) Set y
ys = forall y r.
Ord y =>
N -> LinearCombination r y -> Set y -> Statement
vld N
j (forall r a. Semiring r => SumSymbol r a -> LinearCombination r a
ssylc forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ h (SumSymbol r x) (SumSymbol r y)
h forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
a -> SumSymbol r a
sy x
x) Set y
ys forall b. Boolean b => b -> b -> b
&& forall r (h :: * -> * -> *) x y.
(Semiring r, Commutative r, Hom (Vec r) h, Entity x, Ord x,
 Ord y) =>
h (SumSymbol r x) (SumSymbol r y) -> [(x, N)] -> Set y -> Statement
vlds h (SumSymbol r x) (SumSymbol r y)
h [(x, N)]
xjs Set y
ys

    vld :: Ord y => N -> LinearCombination r y -> Set y -> Statement
    -- as l = h $ sy x the underling lcs l is orderd in the second argument!
    vld :: forall y r.
Ord y =>
N -> LinearCombination r y -> Set y -> Statement
vld N
j LinearCombination r y
l Set y
ys = ((forall x. [x] -> Set x
Set forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall a b. (a, b) -> b
snd forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. LinearCombination r a -> [(r, a)]
lcs LinearCombination r y
l) forall x. Ord x => Set x -> Set x -> Bool
`isSubSet` Set y
ys)
      Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"j"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
j]

--------------------------------------------------------------------------------
-- repMatrix -

repMatricVec :: (Hom (Vec r) h, Entity x, Ord x, Ord y)
  => Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
  -> h (SumSymbol r x) (SumSymbol r y) -> Set x -> Set y -> Matrix r
repMatricVec :: forall r (h :: * -> * -> *) x y.
(Hom (Vec r) h, Entity x, Ord x, Ord y) =>
Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
-> h (SumSymbol r x) (SumSymbol r y) -> Set x -> Set y -> Matrix r
repMatricVec (Struct (Vec r) (SumSymbol r x)
Struct :>: Struct (Vec r) (SumSymbol r y)
Struct) h (SumSymbol r x) (SumSymbol r y)
h Set x
xs Set y
ys = forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim r (Point r)
r Dim r (Point r)
c Entries N N r
ets where
  r :: Dim r (Point r)
r   = forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim forall s. Singleton s => s
unit forall f. Exponential f => f -> Exponent f -> f
^ forall x. LengthN x => x -> N
lengthN Set y
ys
  c :: Dim r (Point r)
c   = forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim forall s. Singleton s => s
unit forall f. Exponential f => f -> Exponent f -> f
^ forall x. LengthN x => x -> N
lengthN Set x
xs
  ets :: Entries N N r
ets = forall i j x. (Ord i, Ord j) => Row j (Col i x) -> Entries i j x
rcets forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x j. (x -> Bool) -> Row j x -> Row j x
rowFilter (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) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r x y.
(Semiring r, Commutative r, Entity x, Ord x) =>
(SumSymbol r x -> SumSymbol r y)
-> (y -> Maybe N) -> [(x, N)] -> Row N (Col N r)
rc (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h (SumSymbol r x) (SumSymbol r y)
h) (forall x. Ord x => Set x -> x -> Maybe N
setIndex Set y
ys) (forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN Set x
xs)

  rc :: (Semiring r, Commutative r, Entity x, Ord x)
    => (SumSymbol r x -> SumSymbol r y) -> (y -> Maybe N) -> [(x,N)] -> Row N (Col N r)
  rc :: forall r x y.
(Semiring r, Commutative r, Entity x, Ord x) =>
(SumSymbol r x -> SumSymbol r y)
-> (y -> Maybe N) -> [(x, N)] -> Row N (Col N r)
rc SumSymbol r x -> SumSymbol r y
h y -> Maybe N
iy = forall j x. PSequence j x -> Row j x
Row forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall i x. [(x, i)] -> PSequence i x
PSequence forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r x y j.
(Semiring r, Commutative r, Entity x, Ord x) =>
(SumSymbol r x -> SumSymbol r y)
-> (y -> Maybe N) -> [(x, j)] -> [(Col N r, j)]
cls SumSymbol r x -> SumSymbol r y
h y -> Maybe N
iy 
    
  cls :: (Semiring r, Commutative r, Entity x, Ord x)
    => (SumSymbol r x -> SumSymbol r y) -> (y -> Maybe N) -> [(x,j)] -> [(Col N r,j)]
  cls :: forall r x y j.
(Semiring r, Commutative r, Entity x, Ord x) =>
(SumSymbol r x -> SumSymbol r y)
-> (y -> Maybe N) -> [(x, j)] -> [(Col N r, j)]
cls SumSymbol r x -> SumSymbol r y
_ y -> Maybe N
_ []           = []
  cls SumSymbol r x -> SumSymbol r y
h y -> Maybe N
iy ((x
x,j
j):[(x, j)]
xjs) = (forall r y.
Semiring r =>
(y -> Maybe N) -> SumSymbol r y -> Col N r
cl y -> Maybe N
iy (SumSymbol r x -> SumSymbol r y
h forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
a -> SumSymbol r a
sy x
x),j
j)forall a. a -> [a] -> [a]
:forall r x y j.
(Semiring r, Commutative r, Entity x, Ord x) =>
(SumSymbol r x -> SumSymbol r y)
-> (y -> Maybe N) -> [(x, j)] -> [(Col N r, j)]
cls SumSymbol r x -> SumSymbol r y
h y -> Maybe N
iy [(x, j)]
xjs

  cl :: Semiring r => (y -> Maybe N) -> SumSymbol r y -> Col N r
  cl :: forall r y.
Semiring r =>
(y -> Maybe N) -> SumSymbol r y -> Col N r
cl y -> Maybe N
iy SumSymbol r y
sy
    = forall i x. PSequence i x -> Col i x
Col
    forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. [(x, i)] -> PSequence i x
PSequence
    forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd
    forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (\(r
r,y
y) -> (r
r,forall a. HasCallStack => Maybe a -> a
fromJust forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ y -> Maybe N
iy y
y))
    forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. LinearCombination r a -> [(r, a)]
lcs
    forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. Semiring r => SumSymbol r a -> LinearCombination r a
ssylc SumSymbol r y
sy


-- | the associated representation matrix of the given @__r__@-homomorphism and the two symbol set.
--
-- __Property__ Let @p = 'Representable' h xs ys@ be in @'Representable' __r__ __h__ __x__ __y__@
-- for a 'Commutative' 'Semiring' @__r__@, then holds:
-- For all @v@ in @'Vector' __r__@ holds: Let @h' = 'HomMatrix' ('repMatrix' p)@ in
--
-- (1) For all @(_,i)@ in @h' '$' v@ holds: @i '<' 'lengthN' ys@.
--
-- (2) @('Ssy' ys '$' h' '$' v) '==' (h '$' 'Ssy' xs '$' v)@.
repMatrix :: Representable r h x y -> Matrix r
repMatrix :: forall r (h :: * -> * -> *) x y. Representable r h x y -> Matrix r
repMatrix (Representable h (SumSymbol r x) (SumSymbol r y)
h Set x
xs Set y
ys) = forall r (h :: * -> * -> *) x y.
(Hom (Vec r) h, Entity x, Ord x, Ord y) =>
Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
-> h (SumSymbol r x) (SumSymbol r y) -> Set x -> Set y -> Matrix r
repMatricVec (forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h (SumSymbol r x) (SumSymbol r y)
h)) h (SumSymbol r x) (SumSymbol r y)
h Set x
xs Set y
ys

--------------------------------------------------------------------------------
-- mtxHomSymbol -

-- | the associated @__r__@-linear homomorphism.
mtxHomSymbol :: Matrix r -> HomSymbol r (SumSymbol r N) (SumSymbol r N)
mtxHomSymbol :: forall r. Matrix r -> HomSymbol r (SumSymbol r N) (SumSymbol r N)
mtxHomSymbol Matrix r
m = forall x y r.
(Entity x, Ord x, Entity y, Ord y) =>
PSequence x (LinearCombination r y)
-> HomSymbol r (SumSymbol r x) (SumSymbol r y)
HomSymbol forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r. Matrix r -> PSequence N (LinearCombination r N)
d Matrix r
m where
  d :: Matrix r -> PSequence N (LinearCombination r N)
  d :: forall r. Matrix r -> PSequence N (LinearCombination r N)
d = forall i x. [(x, i)] -> PSequence i x
PSequence forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall j x. Row j x -> [(x, j)]
rowxs forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall r. Col N r -> LinearCombination r N
collc forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall i j x. (Ord i, Ord j) => Entries i j x -> Row j (Col i x)
etsrc forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. Matrix x -> Entries N N x
mtxxs

  collc :: Col N r -> LinearCombination r N
  collc :: forall r. Col N r -> LinearCombination r N
collc = forall r a. [(r, a)] -> LinearCombination r a
LinearCombination forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall i x. Col i x -> [(x, i)]
colxs
  
--------------------------------------------------------------------------------
-- mtxRepresentable -

-- | the associated representation of a matrix.
mtxRepresentable :: (Semiring r, Commutative r)
  => Matrix r -> Representable r (HomSymbol r) (SumSymbol r N) (SumSymbol r N)
mtxRepresentable :: forall r.
(Semiring r, Commutative r) =>
Matrix r
-> Representable r (HomSymbol r) (SumSymbol r N) (SumSymbol r N)
mtxRepresentable Matrix r
m = forall r (h :: * -> * -> *) x y.
(Hom (Vec r) h, Entity x, Ord x, Entity y, Ord y) =>
h (SumSymbol r x) (SumSymbol r y)
-> Set x
-> Set y
-> Representable r h (SumSymbol r x) (SumSymbol r y)
Representable (forall r. Matrix r -> HomSymbol r (SumSymbol r N) (SumSymbol r N)
mtxHomSymbol Matrix r
m) (forall x. [x] -> Set x
Set [N
0..N
c]) (forall x. [x] -> Set x
Set [N
0..N
r]) where
  c :: N
c = forall x. LengthN x => x -> N
lengthN forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x p. Dim x p -> ProductSymbol p
fromDim forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Matrix x -> Dim' x
cols Matrix r
m
  r :: N
r = forall x. LengthN x => x -> N
lengthN forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x p. Dim x p -> ProductSymbol p
fromDim forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Matrix x -> Dim' x
rows Matrix r
m

--------------------------------------------------------------------------------
-- xVecN -

-- | random variable of @'Vector' __r__@ where all indices are strict smaller then the given bound.
--
-- __Property__ Let @n@ be in 'N' and @xr@ be in @'X' __r__@ then holds:
-- For all @(_,i)@ in the range of @'xVecN' n xr@ holds: @i '<' n@.
xVecN :: Semiring r => N -> X r -> X (Vector r)
xVecN :: forall r. Semiring r => N -> X r -> X (Vector r)
xVecN N
0 X r
_  = forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r. Semiring r => [(r, N)] -> Vector r
vector []
xVecN N
n X r
xr = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall r. Semiring r => [(r, N)] -> Vector r
vector forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> X [(r, N)]
xri N
5 where
  xri :: N -> X [(r, N)]
xri N
m = forall x. N -> N -> X x -> X [x]
xTakeB N
0 (N
mforall c. Multiplicative c => c -> c -> c
*N
n) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. X a -> X b -> X (a, b)
xTupple2 X r
xr (N -> N -> X N
xNB N
0 (forall a. Enum a => a -> a
pred N
n))

dstVecMax :: Semiring r => Int -> N -> X r -> IO ()
dstVecMax :: forall r. Semiring r => Int -> N -> X r -> IO ()
dstVecMax Int
d N
n X r
xr = IO Omega
getOmega forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
d (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall x. LengthN x => x -> N
lengthN forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r. Vector r -> PSequence N r
vecpsq) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r. Semiring r => N -> X r -> X (Vector r)
xVecN N
n X r
xr)

--------------------------------------------------------------------------------
-- prpRepMatrix -

-- | validity of 'repMatrix' for the given vector.
prpRepMatrix :: (Semiring r, Commutative r) => Representable r h x y -> Vector r -> Statement
prpRepMatrix :: forall r (h :: * -> * -> *) x y.
(Semiring r, Commutative r) =>
Representable r h x y -> Vector r -> Statement
prpRepMatrix p :: Representable r h x y
p@(Representable h (SumSymbol r x) (SumSymbol r y)
h Set x
xs Set y
ys) Vector r
v = String -> Label
Prp String
"RepMatrix" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (Closer N
mi forall a. Ord a => a -> a -> Bool
< (forall x. x -> Closer x
It forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. LengthN x => x -> N
lengthN Set y
ys))
          Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h' $ v"String -> String -> Parameter
:=forall a. Show a => a -> String
show Vector r
w,String
"max index"String -> String -> Parameter
:=forall a. Show a => a -> String
show Closer N
mi]
      , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: ((forall x r.
(Entity x, Ord x) =>
Set x -> HomSymbol r (Vector r) (SumSymbol r x)
Ssy Set y
ys forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Vector r
w) forall a. Eq a => a -> a -> Bool
== (h (SumSymbol r x) (SumSymbol r y)
h forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x r.
(Entity x, Ord x) =>
Set x -> HomSymbol r (Vector r) (SumSymbol r x)
Ssy Set x
xs forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Vector r
v))
          Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"p"String -> String -> Parameter
:=forall a. Show a => a -> String
show Representable r h x y
p,String
"h'"String -> String -> Parameter
:=forall a. Show a => a -> String
show HomSymbol r (Vector r) (Vector r)
h',String
"v"String -> String -> Parameter
:=forall a. Show a => a -> String
show Vector r
v]
      ]
  where h' :: HomSymbol r (Vector r) (Vector r)
h' = forall r. Matrix r -> HomSymbol r (Vector r) (Vector r)
HomMatrix forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r (h :: * -> * -> *) x y. Representable r h x y -> Matrix r
repMatrix Representable r h x y
p
        w :: Vector r
w  = HomSymbol r (Vector r) (Vector r)
h' forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Vector r
v
        mi :: Closer N
mi = forall x. Ord x => [x] -> Closer x
cmax forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall a b. (a, b) -> b
snd forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. PSequence i x -> [(x, i)]
psqxs forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r. Vector r -> PSequence N r
vecpsq Vector r
w

--------------------------------------------------------------------------------
-- prpRepMatrixZ -

-- | validity of 'repMatrix' for 'Z'-matrices with the given row and column numbers.
prpRepMatrixZ :: N -> N -> Statement
prpRepMatrixZ :: N -> N -> Statement
prpRepMatrixZ N
n N
m = forall x. X x -> (x -> Statement) -> Statement
Forall X (Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N),
   Vector Z)
xrv (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall r (h :: * -> * -> *) x y.
(Semiring r, Commutative r) =>
Representable r h x y -> Vector r -> Statement
prpRepMatrix) where
  xrv :: X (Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N),
   Vector Z)
xrv = forall a b. X a -> X b -> X (a, b)
xTupple2 X (Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N))
xr X (Vector Z)
xv
  xr :: X (Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N))
xr  = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall r.
(Semiring r, Commutative r) =>
Matrix r
-> Representable r (HomSymbol r) (SumSymbol r N) (SumSymbol r N)
mtxRepresentable forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation (Matrix Z)
xodZ (Dim Z ()
c forall p. p -> p -> Orientation p
:> Dim Z ()
r)
  c :: Dim Z ()
c   = forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim () forall f. Exponential f => f -> Exponent f -> f
^ N
m
  r :: Dim Z ()
r   = forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim () forall f. Exponential f => f -> Exponent f -> f
^ N
n
  xv :: X (Vector Z)
xv  = forall r. Semiring r => N -> X r -> X (Vector r)
xVecN N
m (Z -> Z -> X Z
xZB (-Z
100) Z
100)