Agda.Termination.SparseMatrix

Sparse matrices.

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

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

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

tests :: IO Bool