Agda-2.2.8: A dependently typed functional programming language and proof assistant

Agda.Termination.SparseMatrix

Contents

Description

Sparse matrices.

We assume the matrices to be very sparse, so we just implement them as sorted association lists.

Synopsis

Basic data types

data Matrix i b Source

Type of matrices, parameterised on the type of values.

Instances

(Eq i, Eq b) => Eq (Matrix i b) 
(Ord i, Ord b) => Ord (Matrix i b) 
(Ord i, Integral i, Enum i, Show i, Show b, HasZero b) => Show (Matrix i b) 
(Arbitrary i, Num i, Integral i, Arbitrary b, HasZero b) => Arbitrary (Matrix i b) 
(Ord i, Integral i, Enum i, CoArbitrary b, HasZero b) => CoArbitrary (Matrix i b) 
(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) 

matrixInvariant :: (Num i, Ix i) => Matrix i b -> BoolSource

data Size i Source

Size of a matrix.

Constructors

Size 

Fields

rows :: i
 
cols :: i
 

Instances

Eq i => Eq (Size i) 
Ord i => Ord (Size i) 
Show i => Show (Size i) 
(Arbitrary i, Integral i) => Arbitrary (Size i) 
CoArbitrary i => CoArbitrary (Size i) 

sizeInvariant :: (Ord i, Num i) => Size i -> BoolSource

data MIx i Source

Type of matrix indices (row, column).

Constructors

MIx 

Fields

row :: i
 
col :: i
 

Instances

Eq i => Eq (MIx i) 
Ord i => Ord (MIx i) 
Show i => Show (MIx i) 
Ix i => Ix (MIx i) 
(Arbitrary i, Integral i) => Arbitrary (MIx i) 
CoArbitrary i => CoArbitrary (MIx i) 

mIxInvariant :: (Ord i, Num i) => MIx i -> BoolSource

No nonpositive indices are allowed.

Generating and creating matrices

fromLists :: (Ord i, Num i, Enum i, HasZero b) => Size i -> [[b]] -> Matrix i bSource

fromLists sz rs constructs a matrix from a list of lists of values (a list of rows).

Precondition: length rs == rows sz && all ((== cols sz) . length) rs.

fromIndexList :: (Ord i, HasZero b) => Size i -> [(MIx i, b)] -> Matrix i bSource

Constructs a matrix from a list of (index, value)-pairs.

toLists :: (Ord i, Integral i, Enum i, HasZero b) => Matrix i b -> [[b]]Source

Converts a matrix to a list of row lists.

matrix :: (Arbitrary i, Integral i, Arbitrary b, HasZero b) => Size i -> Gen (Matrix i b)Source

Generates a matrix of the given size.

matrixUsingRowGenSource

Arguments

:: (Arbitrary i, Integral i, Arbitrary b, HasZero b) 
=> Size i 
-> (i -> Gen [b])

The generator is parameterised on the size of the row.

-> Gen (Matrix i b) 

Generates a matrix of the given size, using the given generator to generate the rows.

Combining and querying matrices

size :: Matrix i b -> Size iSource

square :: Ix i => Matrix i b -> BoolSource

True iff the matrix is square.

isEmpty :: (Num i, Ix i) => Matrix i b -> BoolSource

Returns True iff the matrix is empty.

isSingleton :: (Num i, Ix i) => Matrix i b -> Maybe bSource

Returns 'Just b' iff it is a 1x1 matrix with just one entry b.

add :: Ord i => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i aSource

Transposition

add (+) m1 m2 adds m1 and m2. Uses (+) to add values.

Precondition: size m1 == size m2.

intersectWith :: Ord i => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i aSource

intersectWith f m1 m2 build the pointwise conjunction m1 and m2. Uses f to combine non-zero values.

Precondition: size m1 == size m2.

mul :: (Enum i, Num i, Ix i, Eq a) => Semiring a -> Matrix i a -> Matrix i a -> Matrix i aSource

mul semiring m1 m2 multiplies m1 and m2. Uses the operations of the semiring semiring to perform the multiplication.

Precondition: cols (size m1) == rows (size m2).

transpose :: Ord i => Matrix i b -> Matrix i bSource

diagonal :: (Enum i, Num i, Ix i, HasZero b) => Matrix i b -> Array i bSource

diagonal m extracts the diagonal of m.

Precondition: square m.

Modifying matrices

addRow :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i bSource

addRow x m adds a new row to m, after the rows already existing in the matrix. All elements in the new row get set to x.

addColumn :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i bSource

addColumn x m adds a new column to m, after the columns already existing in the matrix. All elements in the new column get set to x.

Tests