{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE 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.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.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
[Vector r] -> ShowS
Vector r -> String
(Int -> Vector r -> ShowS)
-> (Vector r -> String) -> ([Vector r] -> ShowS) -> Show (Vector r)
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
$cshowsPrec :: forall r. Show r => Int -> Vector r -> ShowS
showsPrec :: Int -> Vector r -> ShowS
$cshow :: forall r. Show r => Vector r -> String
show :: Vector r -> String
$cshowList :: forall r. Show r => [Vector r] -> ShowS
showList :: [Vector r] -> ShowS
Show,Vector r -> Vector r -> Bool
(Vector r -> Vector r -> Bool)
-> (Vector r -> Vector r -> Bool) -> Eq (Vector r)
forall r. Eq r => Vector r -> Vector r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Vector r -> Vector r -> Bool
Eq,Eq (Vector r)
Eq (Vector r) =>
(Vector r -> Vector r -> Ordering)
-> (Vector r -> Vector r -> Bool)
-> (Vector r -> Vector r -> Bool)
-> (Vector r -> Vector r -> Bool)
-> (Vector r -> Vector r -> Bool)
-> (Vector r -> Vector r -> Vector r)
-> (Vector r -> Vector r -> Vector r)
-> Ord (Vector r)
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
$ccompare :: forall r. Ord r => Vector r -> Vector r -> Ordering
compare :: Vector r -> Vector r -> Ordering
$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
>= :: Vector r -> Vector r -> Bool
$cmax :: forall r. Ord r => Vector r -> Vector r -> Vector r
max :: Vector r -> Vector r -> Vector r
$cmin :: forall r. Ord r => Vector r -> Vector r -> Vector r
min :: Vector r -> Vector r -> Vector r
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 = PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector (PSequence N r -> Vector r)
-> ([(r, N)] -> PSequence N r) -> [(r, N)] -> Vector r
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
. (r -> Bool) -> PSequence N r -> PSequence N r
forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> (r -> Bool) -> r -> 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
. r -> Bool
forall a. Additive a => a -> Bool
isZero) (PSequence N r -> PSequence N r)
-> ([(r, N)] -> PSequence N r) -> [(r, N)] -> PSequence N r
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
. (r -> r -> r) -> [(r, N)] -> PSequence N r
forall i x. Ord i => (x -> x -> x) -> [(x, i)] -> PSequence i x
psequence r -> r -> r
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 = r -> Maybe r -> r
forall a. a -> Maybe a -> a
fromMaybe r
forall r. Semiring r => r
rZero (PSequence N r
v PSequence N r -> N -> Maybe r
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 (String -> Label) -> String -> Label
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> TypeRep -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Vector r -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Vector r
v) Label -> Statement -> Statement
:<=>: PSequence N r -> Statement
forall {b} {x}.
(Ord b, Additive x, Show b, Validable b, Typeable b) =>
PSequence b x -> Statement
vldVec PSequence N r
ris where
    vldVec :: PSequence b x -> Statement
vldVec PSequence b x
ris
      = [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: PSequence b x -> Statement
forall a. Validable a => a -> Statement
valid PSequence b x
ris
            , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (Statement -> (x, b) -> Statement)
-> Statement -> [(x, b)] -> Statement
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Statement -> (x, b) -> Statement
forall {x} {b}.
(Additive x, Show b) =>
Statement -> (x, b) -> Statement
vldxs Statement
SValid (PSequence b x -> [(x, b)]
forall i x. PSequence i x -> [(x, i)]
psqxs PSequence b x
ris)
            ]

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

-- instance Semiring r => Entity (Vector r)


--------------------------------------------------------------------------------

-- Vector - Euclidean -


type instance Root (Vector r) = ()

instance ShowRoot (Vector r)
instance EqRoot (Vector r)
instance ValidableRoot (Vector r)
instance TypeableRoot (Vector r)

instance Semiring r => Fibred (Vector r) where
  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)
_ = PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector PSequence N r
forall i x. PSequence i x
psqEmpty
  
  Vector PSequence N r
v + :: Vector r -> Vector r -> Vector r
+ Vector PSequence N r
w = PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector ((r -> Bool) -> PSequence N r -> PSequence N r
forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> (r -> Bool) -> r -> 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
. r -> Bool
forall a. Additive a => a -> Bool
isZero) (PSequence N r -> PSequence N r) -> PSequence N r -> PSequence N r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (r -> r -> r)
-> (r -> r)
-> (r -> r)
-> PSequence N r
-> PSequence N r
-> PSequence N r
forall i x y z.
Ord i =>
(x -> y -> z)
-> (x -> z)
-> (y -> z)
-> PSequence i x
-> PSequence i y
-> PSequence i z
psqInterlace r -> r -> r
forall a. Additive a => a -> a -> a
(+) r -> r
forall x. x -> x
id r -> r
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) = PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector ((r -> Bool) -> PSequence N r -> PSequence N r
forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> (r -> Bool) -> r -> 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
. r -> Bool
forall a. Additive a => a -> Bool
isZero) (PSequence N r -> PSequence N r) -> PSequence N r -> PSequence N r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (r -> r) -> PSequence N r -> PSequence N r
forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap (N -> r -> r
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) = PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector ((r -> r) -> PSequence N r -> PSequence N r
forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap r -> r
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) = PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector ((r -> Bool) -> PSequence N r -> PSequence N r
forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> (r -> Bool) -> r -> 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
. r -> Bool
forall a. Additive a => a -> Bool
isZero) (PSequence N r -> PSequence N r) -> PSequence N r -> PSequence N r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (r -> r) -> PSequence N r -> PSequence N r
forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap (Z -> r -> r
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) = PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector ((r -> Bool) -> PSequence N r -> PSequence N r
forall x i. (x -> Bool) -> PSequence i x -> PSequence i x
psqFilter (Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> (r -> Bool) -> r -> 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
. r -> Bool
forall a. Additive a => a -> Bool
isZero) (PSequence N r -> PSequence N r) -> PSequence N r -> PSequence N r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (r -> r) -> PSequence N r -> PSequence N r
forall x y i. (x -> y) -> PSequence i x -> PSequence i y
psqMap (r
Scalar (Vector r)
rr -> r -> r
forall 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
    = (r -> r -> r) -> r -> [r] -> r
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl r -> r -> r
forall a. Additive a => a -> a -> a
(+) r
forall r. Semiring r => r
rZero
    ([r] -> r) -> [r] -> r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((r, N) -> r) -> [(r, N)] -> [r]
forall a b. (a -> b) -> [a] -> [b]
map (r, N) -> r
forall a b. (a, b) -> a
fst
    ([(r, N)] -> [r]) -> [(r, N)] -> [r]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence N r -> [(r, N)]
forall i x. PSequence i x -> [(x, i)]
psqxs
    (PSequence N r -> [(r, N)]) -> PSequence N r -> [(r, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (r -> r -> r)
-> (r -> r)
-> (r -> r)
-> PSequence N r
-> PSequence N r
-> PSequence N r
forall i x y z.
Ord i =>
(x -> y -> z)
-> (x -> z)
-> (y -> z)
-> PSequence i x
-> PSequence i y
-> PSequence i z
psqInterlace r -> r -> r
forall c. Multiplicative c => c -> c -> c
(*) (r -> r -> r
forall b a. b -> a -> b
const r
forall r. Semiring r => r
rZero) (r -> r -> r
forall b a. b -> a -> b
const r
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 = PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector (PSequence a r -> PSequence N a -> PSequence N r
forall i j x.
(Ord i, Ord j) =>
PSequence i x -> PSequence j i -> PSequence j x
psqCompose ([(r, a)] -> PSequence a r
forall i x. [(x, i)] -> PSequence i x
PSequence ([(r, a)] -> PSequence a r) -> [(r, a)] -> PSequence a r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LinearCombination r a -> [(r, a)]
forall r a. LinearCombination r a -> [(r, a)]
lcs (LinearCombination r a -> [(r, a)])
-> LinearCombination r a -> [(r, a)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SumSymbol r a -> LinearCombination r a
forall r a. Semiring r => SumSymbol r a -> LinearCombination r a
ssylc SumSymbol r a
x) ([(a, N)] -> PSequence N a
forall i x. [(x, i)] -> PSequence i x
PSequence ([(a, N)] -> PSequence N a) -> [(a, N)] -> PSequence N a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Set a -> [(a, N)]
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:

--

-- (1) @'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 = [(r, a)] -> SumSymbol r a
forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
[(r, a)] -> SumSymbol r a
sumSymbol ([(r, a)] -> SumSymbol r a) -> [(r, a)] -> SumSymbol r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence a r -> [(r, a)]
forall i x. PSequence i x -> [(x, i)]
psqxs (PSequence a r -> [(r, a)]) -> PSequence a r -> [(r, a)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence N r -> PSequence a N -> PSequence a r
forall i j x.
(Ord i, Ord j) =>
PSequence i x -> PSequence j i -> PSequence j x
psqCompose (Vector r -> PSequence N r
forall r. Vector r -> PSequence N r
vecpsq Vector r
v) ([(N, a)] -> PSequence a N
forall i x. [(x, i)] -> PSequence i x
PSequence ([(N, a)] -> PSequence a N) -> [(N, a)] -> PSequence a N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((a, N) -> (N, a)) -> [(a, N)] -> [(N, a)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
a,N
i) -> (N
i,a
a)) ([(a, N)] -> [(N, a)]) -> [(a, N)] -> [(N, a)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Set a -> [(a, N)]
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 []))  = Row N (Col N r)
forall j x. Row j x
rowEmpty
vecrc (Vector PSequence N r
v)               = PSequence N (Col N r) -> Row N (Col N r)
forall j x. PSequence j x -> Row j x
Row (PSequence N (Col N r) -> Row N (Col N r))
-> PSequence N (Col N r) -> Row N (Col N r)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Col N r, N)] -> PSequence N (Col N r)
forall i x. [(x, i)] -> PSequence i x
PSequence [(PSequence N r -> Col N r
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 = Col N (Row N r) -> Vector r
forall r. Col N (Row N r) -> Vector r
crvec (Matrix r -> Col N (Row N r)
forall x. Matrix x -> Col N (Row N x)
mtxColRow Matrix r
m Col N (Row N r) -> Row N (Col N r) -> Col N (Row N r)
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` Vector r -> Row N (Col N r)
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 N -> Col N (Row N r) -> Col N r
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 -> PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector PSequence N r
v

--------------------------------------------------------------------------------

-- HomSymbol -


-- | homomorphisms 'Vector' and symbolic sums 'SumSymbol'.

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
:<=>: PSequence x (LinearCombination r y) -> 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
:<=>: Set x -> Statement
forall a. Validable a => a -> Statement
valid Set x
xs
    Ssy Set x
xs        -> String -> Label
Label String
"Ssy" Label -> Statement -> Statement
:<=>: Set x -> Statement
forall a. Validable a => a -> Statement
valid Set x
xs
    HomMatrix Matrix r
m   -> String -> Label
Label String
"HomMatrix" Label -> Statement -> Statement
:<=>: Matrix r -> 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) => ApplicativeG Id (HomSymbol r) (->) where
  amapG :: forall x y. HomSymbol r x y -> Id x -> Id y
amapG (HomSymbol PSequence x (LinearCombination r y)
lcs) (Id x
s) = SumSymbol r y -> Id y
SumSymbol r y -> Id (SumSymbol r y)
forall x. x -> Id x
Id (SumSymbol r y -> Id y) -> SumSymbol r y -> Id y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (x -> LinearCombination r y) -> SumSymbol r x -> SumSymbol r y
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 x
SumSymbol r x
s where
    f :: x -> LinearCombination r y
f x
x = case PSequence x (LinearCombination r y)
lcs PSequence x (LinearCombination r y)
-> x -> Maybe (LinearCombination r y)
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 -> [(r, y)] -> LinearCombination r y
forall r a. [(r, a)] -> LinearCombination r a
LinearCombination []      
  amapG (Cfs Set x
xs) (Id x
s) = Vector r -> Id y
Vector r -> Id (Vector r)
forall x. x -> Id x
Id (Vector r -> Id y) -> Vector r -> Id y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Set x -> SumSymbol r x -> Vector r
forall r a.
(Semiring r, Ord a) =>
Set a -> SumSymbol r a -> Vector r
ssycfs Set x
xs x
SumSymbol r x
s
  amapG (Ssy Set x
xs) (Id x
v) = SumSymbol r x -> Id y
SumSymbol r x -> Id (SumSymbol r x)
forall x. x -> Id x
Id (SumSymbol r x -> Id y) -> SumSymbol r x -> Id y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Set x -> Vector r -> SumSymbol r x
forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
Set a -> Vector r -> SumSymbol r a
cfsssy Set x
xs x
Vector r
v
  amapG (HomMatrix Matrix r
m) (Id x
v) = Vector r -> Id y
Vector r -> Id (Vector r)
forall x. x -> Id x
Id (Vector r -> Id y) -> Vector r -> Id y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Matrix r -> Vector r -> Vector r
forall r. Semiring r => Matrix r -> Vector r -> Vector r
vecAppl Matrix r
m x
Vector r
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)
_ -> Struct (Vec r) x
forall s x. Structure s x => Struct s x
Struct Struct (Vec r) x -> Struct (Vec r) y -> Homomorphous (Vec r) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (Vec r) y
forall s x. Structure s x => Struct s x
Struct
    Cfs Set x
_       -> Struct (Vec r) x
forall s x. Structure s x => Struct s x
Struct Struct (Vec r) x -> Struct (Vec r) y -> Homomorphous (Vec r) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (Vec r) y
forall s x. Structure s x => Struct s x
Struct
    Ssy Set x
_       -> Struct (Vec r) x
forall s x. Structure s x => Struct s x
Struct Struct (Vec r) x -> Struct (Vec r) y -> Homomorphous (Vec r) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (Vec r) y
forall s x. Structure s x => Struct s x
Struct
    HomMatrix Matrix r
_ -> Struct (Vec r) x
forall s x. Structure s x => Struct s x
Struct Struct (Vec r) x -> Struct (Vec r) y -> Homomorphous (Vec r) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (Vec r) y
forall s x. Structure s x => Struct s x
Struct

instance ApplicativeG Rt (HomSymbol r) (->) where
  amapG :: forall x y. HomSymbol r x y -> Rt x -> Rt y
amapG (HomSymbol PSequence x (LinearCombination r y)
_) = (Root x -> Root y) -> Rt x -> Rt y
forall x y. (Root x -> Root y) -> Rt x -> Rt y
amapRt (() -> () -> ()
forall b a. b -> a -> b
const ())
  amapG (Cfs Set x
_)       = (Root x -> Root y) -> Rt x -> Rt y
forall x y. (Root x -> Root y) -> Rt x -> Rt y
amapRt (() -> () -> ()
forall b a. b -> a -> b
const ())
  amapG (Ssy Set x
_)       = (Root x -> Root y) -> Rt x -> Rt y
forall x y. (Root x -> Root y) -> Rt x -> Rt y
amapRt (() -> () -> ()
forall b a. b -> a -> b
const ())
  amapG (HomMatrix Matrix r
_) = (Root x -> Root y) -> Rt x -> Rt y
forall x y. (Root x -> Root y) -> Rt x -> Rt y
amapRt (() -> () -> ()
forall b a. b -> a -> b
const ())

instance (Semiring r, Commutative r) => HomFibred (HomSymbol r) where


instance (Semiring r, Commutative r) => HomAdditive (HomSymbol 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 :: (HomVectorial 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 Show2 h => 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 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ h (SumSymbol r x) (SumSymbol r y) -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h (SumSymbol r x) (SumSymbol r y)
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set x -> String
forall a. Show a => a -> String
show Set x
xs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set y -> String
forall a. Show a => a -> String
show Set y
ys String -> ShowS
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
:<=>: Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
-> h (SumSymbol r x) (SumSymbol r y) -> Set x -> Set y -> Statement
forall r (h :: * -> * -> *) x y.
(HomVectorial 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 (Homomorphous (ObjectClass h) (SumSymbol r x) (SumSymbol r y)
-> Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h (SumSymbol r x) (SumSymbol r y)
-> Homomorphous (ObjectClass h) (SumSymbol r x) (SumSymbol r y)
forall x y. h x y -> Homomorphous (ObjectClass h) x y
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 :: (HomVectorial 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.
(HomVectorial 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 = h (SumSymbol r x) (SumSymbol r y) -> [(x, N)] -> Set y -> Statement
forall r (h :: * -> * -> *) x y.
(Semiring r, Commutative r, HomVectorial 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 (Set x -> [(x, N)]
forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN Set x
xs) Set y
ys

    vlds :: (Semiring r, Commutative r, HomVectorial 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, HomVectorial 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 = N -> LinearCombination r y -> Set y -> Statement
forall y r.
Ord y =>
N -> LinearCombination r y -> Set y -> Statement
vld N
j (SumSymbol r y -> LinearCombination r y
forall r a. Semiring r => SumSymbol r a -> LinearCombination r a
ssylc (SumSymbol r y -> LinearCombination r y)
-> SumSymbol r y -> LinearCombination r y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h (SumSymbol r x) (SumSymbol r y)
h h (SumSymbol r x) (SumSymbol r y) -> SumSymbol r x -> SumSymbol r y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ x -> SumSymbol r x
forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
a -> SumSymbol r a
sy x
x) Set y
ys Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& h (SumSymbol r x) (SumSymbol r y) -> [(x, N)] -> Set y -> Statement
forall r (h :: * -> * -> *) x y.
(Semiring r, Commutative r, HomVectorial 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 = (([y] -> Set y
forall x. [x] -> Set x
Set ([y] -> Set y) -> [y] -> Set y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((r, y) -> y) -> [(r, y)] -> [y]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (r, y) -> y
forall a b. (a, b) -> b
snd ([(r, y)] -> [y]) -> [(r, y)] -> [y]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LinearCombination r y -> [(r, y)]
forall r a. LinearCombination r a -> [(r, a)]
lcs LinearCombination r y
l) Set y -> Set y -> Bool
forall x. Ord x => Set x -> Set x -> Bool
`isSubSet` Set y
ys)
      Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"j"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
j]

--------------------------------------------------------------------------------

-- repMatrix -


repMatricVec :: (HomVectorial 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.
(HomVectorial 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 = Dim r (Point r) -> Dim r (Point r) -> Entries N N r -> Matrix r
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   = Point r -> Dim r (Point r)
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim Point r
forall s. Singleton s => s
unit Dim r (Point r) -> Exponent (Dim r (Point r)) -> Dim r (Point r)
forall f. Exponential f => f -> Exponent f -> f
^ Set y -> N
forall x. LengthN x => x -> N
lengthN Set y
ys
  c :: Dim r (Point r)
c   = Point r -> Dim r (Point r)
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim Point r
forall s. Singleton s => s
unit Dim r (Point r) -> Exponent (Dim r (Point r)) -> Dim r (Point r)
forall f. Exponential f => f -> Exponent f -> f
^ Set x -> N
forall x. LengthN x => x -> N
lengthN Set x
xs
  ets :: Entries N N r
ets = Row N (Col N r) -> Entries N N r
forall i j x. (Ord i, Ord j) => Row j (Col i x) -> Entries i j x
rcets (Row N (Col N r) -> Entries N N r)
-> Row N (Col N r) -> Entries N N r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Col N r -> Bool) -> Row N (Col N r) -> Row N (Col N r)
forall x j. (x -> Bool) -> Row j x -> Row j x
rowFilter (Bool -> Bool
forall b. Boolean b => b -> b
not(Bool -> Bool) -> (Col N r -> Bool) -> Col N r -> 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 N r -> Bool
forall i x. Col i x -> Bool
colIsEmpty) (Row N (Col N r) -> Row N (Col N r))
-> Row N (Col N r) -> Row N (Col N r)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (SumSymbol r x -> SumSymbol r y)
-> (y -> Maybe N) -> [(x, N)] -> Row N (Col N r)
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 (h (SumSymbol r x) (SumSymbol r y) -> SumSymbol r x -> SumSymbol r y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h (SumSymbol r x) (SumSymbol r y)
h) (Set y -> y -> Maybe N
forall x. Ord x => Set x -> x -> Maybe N
setIndex Set y
ys) (Set x -> [(x, N)]
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 = PSequence N (Col N r) -> Row N (Col N r)
forall j x. PSequence j x -> Row j x
Row (PSequence N (Col N r) -> Row N (Col N r))
-> ([(x, N)] -> PSequence N (Col N r))
-> [(x, N)]
-> Row N (Col N r)
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 N r, N)] -> PSequence N (Col N r)
forall i x. [(x, i)] -> PSequence i x
PSequence ([(Col N r, N)] -> PSequence N (Col N r))
-> ([(x, N)] -> [(Col N r, N)])
-> [(x, N)]
-> PSequence N (Col N r)
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
. (SumSymbol r x -> SumSymbol r y)
-> (y -> Maybe N) -> [(x, N)] -> [(Col N r, N)]
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) = ((y -> Maybe N) -> SumSymbol r y -> Col N r
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 (SumSymbol r x -> SumSymbol r y) -> SumSymbol r x -> SumSymbol r y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ x -> SumSymbol r x
forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
a -> SumSymbol r a
sy x
x),j
j)(Col N r, j) -> [(Col N r, j)] -> [(Col N r, j)]
forall a. a -> [a] -> [a]
:(SumSymbol r x -> SumSymbol r y)
-> (y -> Maybe N) -> [(x, j)] -> [(Col N r, j)]
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
    = PSequence N r -> Col N r
forall i x. PSequence i x -> Col i x
Col
    (PSequence N r -> Col N r) -> PSequence N r -> Col N r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(r, N)] -> PSequence N r
forall i x. [(x, i)] -> PSequence i x
PSequence
    ([(r, N)] -> PSequence N r) -> [(r, N)] -> PSequence N r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(r, N)] -> [(r, N)]
forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd
    ([(r, N)] -> [(r, N)]) -> [(r, N)] -> [(r, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((r, y) -> (r, N)) -> [(r, y)] -> [(r, N)]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(r
r,y
y) -> (r
r,Maybe N -> N
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe N -> N) -> Maybe N -> N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ y -> Maybe N
iy y
y))
    ([(r, y)] -> [(r, N)]) -> [(r, y)] -> [(r, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LinearCombination r y -> [(r, y)]
forall r a. LinearCombination r a -> [(r, a)]
lcs
    (LinearCombination r y -> [(r, y)])
-> LinearCombination r y -> [(r, y)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SumSymbol r y -> LinearCombination r y
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) = Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
-> h (SumSymbol r x) (SumSymbol r y) -> Set x -> Set y -> Matrix r
forall r (h :: * -> * -> *) x y.
(HomVectorial 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 (Homomorphous (ObjectClass h) (SumSymbol r x) (SumSymbol r y)
-> Homomorphous (Vec r) (SumSymbol r x) (SumSymbol r y)
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h (SumSymbol r x) (SumSymbol r y)
-> Homomorphous (ObjectClass h) (SumSymbol r x) (SumSymbol r y)
forall x y. h x y -> Homomorphous (ObjectClass h) x y
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 = PSequence N (LinearCombination r N)
-> HomSymbol r (SumSymbol r N) (SumSymbol r N)
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 (PSequence N (LinearCombination r N)
 -> HomSymbol r (SumSymbol r N) (SumSymbol r N))
-> PSequence N (LinearCombination r N)
-> HomSymbol r (SumSymbol r N) (SumSymbol r N)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Matrix r -> PSequence N (LinearCombination r N)
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 = [(LinearCombination r N, N)] -> PSequence N (LinearCombination r N)
forall i x. [(x, i)] -> PSequence i x
PSequence ([(LinearCombination r N, N)]
 -> PSequence N (LinearCombination r N))
-> (Matrix r -> [(LinearCombination r N, N)])
-> Matrix r
-> PSequence N (LinearCombination r N)
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 N (LinearCombination r N) -> [(LinearCombination r N, N)]
forall j x. Row j x -> [(x, j)]
rowxs (Row N (LinearCombination r N) -> [(LinearCombination r N, N)])
-> (Matrix r -> Row N (LinearCombination r N))
-> Matrix r
-> [(LinearCombination r N, N)]
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 N r -> LinearCombination r N)
-> Row N (Col N r) -> Row N (LinearCombination r N)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Col N r -> LinearCombination r N
forall r. Col N r -> LinearCombination r N
collc (Row N (Col N r) -> Row N (LinearCombination r N))
-> (Matrix r -> Row N (Col N r))
-> Matrix r
-> Row N (LinearCombination r N)
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
. Entries N N r -> Row N (Col N r)
forall i j x. (Ord i, Ord j) => Entries i j x -> Row j (Col i x)
etsrc (Entries N N r -> Row N (Col N r))
-> (Matrix r -> Entries N N r) -> Matrix r -> Row N (Col N r)
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 r -> Entries N N r
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 = [(r, N)] -> LinearCombination r N
forall r a. [(r, a)] -> LinearCombination r a
LinearCombination ([(r, N)] -> LinearCombination r N)
-> (Col N r -> [(r, N)]) -> Col N r -> LinearCombination r N
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 N r -> [(r, N)]
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 = HomSymbol r (SumSymbol r N) (SumSymbol r N)
-> Set N
-> Set N
-> Representable r (HomSymbol r) (SumSymbol r N) (SumSymbol r N)
forall r (h :: * -> * -> *) x y.
(HomVectorial 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 (Matrix r -> HomSymbol r (SumSymbol r N) (SumSymbol r N)
forall r. Matrix r -> HomSymbol r (SumSymbol r N) (SumSymbol r N)
mtxHomSymbol Matrix r
m) ([N] -> Set N
forall x. [x] -> Set x
Set [N
0..N
c]) ([N] -> Set N
forall x. [x] -> Set x
Set [N
0..N
r]) where
  c :: N
c = ProductSymbol (Point r) -> N
forall x. LengthN x => x -> N
lengthN (ProductSymbol (Point r) -> N) -> ProductSymbol (Point r) -> N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim r (Point r) -> ProductSymbol (Point r)
forall x p. Dim x p -> ProductSymbol p
fromDim (Dim r (Point r) -> ProductSymbol (Point r))
-> Dim r (Point r) -> ProductSymbol (Point r)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Matrix r -> Dim r (Point r)
forall x. Matrix x -> Dim' x
cols Matrix r
m
  r :: N
r = ProductSymbol (Point r) -> N
forall x. LengthN x => x -> N
lengthN (ProductSymbol (Point r) -> N) -> ProductSymbol (Point r) -> N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim r (Point r) -> ProductSymbol (Point r)
forall x p. Dim x p -> ProductSymbol p
fromDim (Dim r (Point r) -> ProductSymbol (Point r))
-> Dim r (Point r) -> ProductSymbol (Point r)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Matrix r -> Dim r (Point r)
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
_  = Vector r -> X (Vector r)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Vector r -> X (Vector r)) -> Vector r -> X (Vector r)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(r, N)] -> Vector r
forall r. Semiring r => [(r, N)] -> Vector r
vector []
xVecN N
n X r
xr = ([(r, N)] -> Vector r) -> X [(r, N)] -> X (Vector r)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 [(r, N)] -> Vector r
forall r. Semiring r => [(r, N)] -> Vector r
vector (X [(r, N)] -> X (Vector r)) -> X [(r, N)] -> X (Vector r)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> X [(r, N)]
xri N
5 where
  xri :: N -> X [(r, N)]
xri N
m = N -> N -> X (r, N) -> X [(r, N)]
forall x. N -> N -> X x -> X [x]
xTakeB N
0 (N
mN -> N -> N
forall c. Multiplicative c => c -> c -> c
*N
n) (X (r, N) -> X [(r, N)]) -> X (r, N) -> X [(r, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X r -> X N -> X (r, N)
forall a b. X a -> X b -> X (a, b)
xTupple2 X r
xr (N -> N -> X N
xNB N
0 (N -> N
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 IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X N -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
d ((Vector r -> N) -> X (Vector r) -> X N
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (PSequence N r -> N
forall x. LengthN x => x -> N
lengthN (PSequence N r -> N)
-> (Vector r -> PSequence N r) -> Vector r -> N
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
. Vector r -> PSequence N r
forall r. Vector r -> PSequence N r
vecpsq) (X (Vector r) -> X N) -> X (Vector r) -> X N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> X r -> X (Vector r)
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, Show2 h) => Representable r h x y -> Vector r -> Statement
prpRepMatrix :: forall r (h :: * -> * -> *) x y.
(Semiring r, Commutative r, Show2 h) =>
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
:<=>: (Closure N
mi Closure N -> Closure N -> Bool
forall a. Ord a => a -> a -> Bool
< (N -> Closure N
forall x. x -> Closure x
It (N -> Closure N) -> N -> Closure N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Set y -> N
forall x. LengthN x => x -> N
lengthN Set y
ys))
          Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h' $ v"String -> String -> Parameter
:=Vector r -> String
forall a. Show a => a -> String
show Vector r
w,String
"max index"String -> String -> Parameter
:=Closure N -> String
forall a. Show a => a -> String
show Closure N
mi]
      , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: ((Set y -> HomSymbol r (Vector r) (SumSymbol r y)
forall x r.
(Entity x, Ord x) =>
Set x -> HomSymbol r (Vector r) (SumSymbol r x)
Ssy Set y
ys HomSymbol r (Vector r) (SumSymbol r y) -> Vector r -> SumSymbol r y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Vector r
w) SumSymbol r y -> SumSymbol r y -> Bool
forall a. Eq a => a -> a -> Bool
== (h (SumSymbol r x) (SumSymbol r y)
h h (SumSymbol r x) (SumSymbol r y) -> SumSymbol r x -> SumSymbol r y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Set x -> HomSymbol r (Vector r) (SumSymbol r x)
forall x r.
(Entity x, Ord x) =>
Set x -> HomSymbol r (Vector r) (SumSymbol r x)
Ssy Set x
xs HomSymbol r (Vector r) (SumSymbol r x) -> Vector r -> SumSymbol r x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Vector r
v))
          Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"p"String -> String -> Parameter
:=Representable r h x y -> String
forall a. Show a => a -> String
show Representable r h x y
p,String
"h'"String -> String -> Parameter
:=HomSymbol r (Vector r) (Vector r) -> String
forall a. Show a => a -> String
show HomSymbol r (Vector r) (Vector r)
h',String
"v"String -> String -> Parameter
:=Vector r -> String
forall a. Show a => a -> String
show Vector r
v]
      ]
  where h' :: HomSymbol r (Vector r) (Vector r)
h' = Matrix r -> HomSymbol r (Vector r) (Vector r)
forall r. Matrix r -> HomSymbol r (Vector r) (Vector r)
HomMatrix (Matrix r -> HomSymbol r (Vector r) (Vector r))
-> Matrix r -> HomSymbol r (Vector r) (Vector r)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Representable r h x y -> Matrix r
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' HomSymbol r (Vector r) (Vector r) -> Vector r -> Vector r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Vector r
v
        mi :: Closure N
mi = [N] -> Closure N
forall x. Ord x => [x] -> Closure x
cmax ([N] -> Closure N) -> [N] -> Closure N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((r, N) -> N) -> [(r, N)] -> [N]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (r, N) -> N
forall a b. (a, b) -> b
snd ([(r, N)] -> [N]) -> [(r, N)] -> [N]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence N r -> [(r, N)]
forall i x. PSequence i x -> [(x, i)]
psqxs (PSequence N r -> [(r, N)]) -> PSequence N r -> [(r, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Vector r -> PSequence N r
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 = X (Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N),
   Vector Z)
-> ((Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N),
     Vector Z)
    -> Statement)
-> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N),
   Vector Z)
xrv ((Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N)
 -> Vector Z -> Statement)
-> (Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N),
    Vector Z)
-> Statement
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N)
-> Vector Z -> Statement
forall r (h :: * -> * -> *) x y.
(Semiring r, Commutative r, Show2 h) =>
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 = X (Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N))
-> X (Vector Z)
-> X (Representable
        Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N),
      Vector Z)
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  = (Matrix Z
 -> Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N))
-> X (Matrix Z)
-> X (Representable
        Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Matrix Z
-> Representable Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N)
forall r.
(Semiring r, Commutative r) =>
Matrix r
-> Representable r (HomSymbol r) (SumSymbol r N) (SumSymbol r N)
mtxRepresentable (X (Matrix Z)
 -> X (Representable
         Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N)))
-> X (Matrix Z)
-> X (Representable
        Z (HomSymbol Z) (SumSymbol Z N) (SumSymbol Z N))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtOrientation (Matrix Z)
-> Orientation (Point (Matrix Z)) -> X (Matrix Z)
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation (Matrix Z)
xodZ (Dim Z ()
c Dim Z () -> Dim Z () -> Orientation (Dim Z ())
forall p. p -> p -> Orientation p
:> Dim Z ()
r)
  c :: Dim Z ()
c   = () -> Dim Z ()
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim () Dim Z () -> Exponent (Dim Z ()) -> Dim Z ()
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (Dim Z ())
m
  r :: Dim Z ()
r   = () -> Dim Z ()
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim () Dim Z () -> Exponent (Dim Z ()) -> Dim Z ()
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (Dim Z ())
n
  xv :: X (Vector Z)
xv  = N -> X Z -> X (Vector Z)
forall r. Semiring r => N -> X r -> X (Vector r)
xVecN N
m (Z -> Z -> X Z
xZB (-Z
100) Z
100)