Agda-2.3.0: 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

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) 
(Show i, Ord i, Integral i, Enum i, CoArbitrary b, HasZero b) => CoArbitrary (Matrix i b) 
(Show i, Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) 

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

data Size i

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 -> Bool

data MIx i

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 -> Bool

No nonpositive indices are allowed.

Generating and creating matrices

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

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 b

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

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

Converts a matrix to a list of row lists.

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

Generates a matrix of the given size.

matrixUsingRowGen

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 i

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

True iff the matrix is square.

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

Returns True iff the matrix is empty.

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

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 a

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 a

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 a

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 b

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

diagonal m extracts the diagonal of m.

Precondition: square m.

Modifying matrices

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

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 b

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