|
Agda.Termination.SparseMatrix |
|
|
|
|
Description |
Sparse matrices.
We assume the matrices to be very sparse, so we just implement them as
sorted association lists.
|
|
Synopsis |
|
data Matrix i b | | matrixInvariant :: (Num i, Ix i) => Matrix i b -> Bool | | data Size i = Size {} | | sizeInvariant :: (Ord i, Num i) => Size i -> Bool | | data MIx i = MIx {} | | mIxInvariant :: (Ord i, Num i) => MIx i -> Bool | | fromLists :: (Ord i, Num i, Enum i, HasZero b) => Size i -> [[b]] -> Matrix i b | | fromIndexList :: (Ord i, HasZero b) => Size i -> [(MIx i, b)] -> Matrix i b | | toLists :: (Ord i, Integral i, Enum i, HasZero b) => Matrix i b -> [[b]] | | matrix :: (Arbitrary i, Integral i, Arbitrary b, HasZero b) => Size i -> Gen (Matrix i b) | | matrixUsingRowGen :: (Arbitrary i, Integral i, Arbitrary b, HasZero b) => Size i -> (i -> Gen [b]) -> Gen (Matrix i b) | | size :: Matrix i b -> Size i | | square :: Ix i => Matrix i b -> Bool | | isEmpty :: (Num i, Ix i) => Matrix i b -> Bool | | isSingleton :: (Num i, Ix i) => Matrix i b -> Maybe b | | add :: Ord i => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a | | intersectWith :: Ord i => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a | | mul :: (Enum i, Num i, Ix i, Eq a) => Semiring a -> Matrix i a -> Matrix i a -> Matrix i a | | transpose :: Ord i => Matrix i b -> Matrix i b | | diagonal :: (Enum i, Num i, Ix i, HasZero b) => Matrix i b -> Array i b | | addRow :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b | | addColumn :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b | | tests :: IO Bool |
|
|
|
Basic data types
|
|
|
Type of matrices, parameterised on the type of values.
|
|
|
|
|
|
Size of a matrix.
| Constructors | |
|
|
|
|
|
Type of matrix indices (row, column).
| Constructors | |
|
|
|
No nonpositive indices are allowed.
|
|
Generating and creating matrices
|
|
|
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.
|
|
|
Constructs a matrix from a list of (index, value)-pairs.
|
|
|
Converts a matrix to a list of row lists.
|
|
|
Generates a matrix of the given size.
|
|
|
|
|
Combining and querying matrices
|
|
|
|
|
True iff the matrix is square.
|
|
|
Returns True iff the matrix is empty.
|
|
|
Returns 'Just b' iff it is a 1x1 matrix with just one entry b.
|
|
|
Transposition
add (+) m1 m2 adds m1 and m2. Uses (+) to add values.
Precondition: size m1 == size m2.
|
|
|
intersectWith f m1 m2 build the pointwise conjunction m1 and m2.
Uses f to combine non-zero values.
Precondition: size m1 == size m2.
|
|
|
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).
|
|
|
|
|
diagonal m extracts the diagonal of m.
Precondition: square m.
|
|
Modifying matrices
|
|
|
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 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
|
|
|
|
Produced by Haddock version 2.6.1 |