Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Termination.Matrix
Contents
Basic data types
Generating and creating matrices
Combining and querying matrices
Modifying matrices
Tests
Description
Naive implementation of simple matrix library.
Synopsis
data Matrix i b
matrixInvariant :: (Num i, Ix i) => Matrix i b -> Bool
data Size i = Size {
rows :: i
cols :: i
}
sizeInvariant :: (Ord i, Num i) => Size i -> Bool
data MIx i = MIx {
row :: i
col :: i
}
mIxInvariant :: (Ord i, Num i) => MIx i -> Bool
fromLists :: (Num i, Ix i) => Size i -> [[b]] -> Matrix i b
fromIndexList :: (Num i, Ix i) => Size i -> [(MIx i, b)] -> Matrix i b
toLists :: (Ix i, Num i, Enum i) => Matrix i b -> [[b]]
zipWith :: (a -> b -> c) -> Matrix Integer a -> Matrix Integer b -> Matrix Integer c
matrix :: (Arbitrary i, Integral i, Ix i, Arbitrary b) => Size i -> Gen (Matrix i b)
matrixUsingRowGen :: (Arbitrary i, Integral i, Ix i, Arbitrary b) => Size i -> (i -> Gen [b]) -> Gen (Matrix i b)
size :: Ix i => Matrix i b -> Size i
square :: Ix i => Matrix i b -> Bool
isEmpty :: (Num i, Ix i) => Matrix i b -> Bool
add :: (Ix i, Num i) => (a -> b -> c) -> Matrix i a -> Matrix i b -> Matrix i c
mul :: (Enum i, Num i, Ix i) => Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
diagonal :: (Enum i, Num i, Ix i) => Matrix i b -> Array i b
addRow :: (Ix i, Integral i) => b -> Matrix i b -> Matrix i b
addColumn :: (Ix i, Num i, Enum i) => b -> Matrix i b -> Matrix i b
tests :: IO Bool
Basic data types
data Matrix i b Source
Type of matrices, parameterised on the type of values.
matrixInvariant :: (Num i, Ix i) => Matrix i b -> BoolSource
data Size i Source
Size of a matrix.
Constructors
Size
rows :: i
cols :: i
sizeInvariant :: (Ord i, Num i) => Size i -> BoolSource
data MIx i Source
Type of matrix indices (row, column).
Constructors
MIx
row :: i
col :: i
mIxInvariant :: (Ord i, Num i) => MIx i -> BoolSource
No nonpositive indices are allowed.
Generating and creating matrices
fromLists :: (Num i, Ix i) => 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 :: (Num i, Ix i) => Size i -> [(MIx i, b)] -> Matrix i bSource
Constructs a matrix from a list of (index, value)-pairs.
toLists :: (Ix i, Num i, Enum i) => Matrix i b -> [[b]]Source
Converts a matrix to a list of row lists.
zipWith :: (a -> b -> c) -> Matrix Integer a -> Matrix Integer b -> Matrix Integer cSource
matrix :: (Arbitrary i, Integral i, Ix i, Arbitrary b) => Size i -> Gen (Matrix i b)Source
Generates a matrix of the given size.
matrixUsingRowGenSource
:: (Arbitrary i, Integral i, Ix i, Arbitrary b)
=> Size iThe generator is parameterised on the size of the row.
-> i -> Gen [b]
-> Gen (Matrix i b)
Generates a matrix of the given size, using the given generator to generate the rows.
Combining and querying matrices
size :: Ix i => Matrix i b -> Size iSource
The size of a matrix.
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.
add :: (Ix i, Num i) => (a -> b -> c) -> Matrix i a -> Matrix i b -> Matrix i cSource

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

Precondition: size m1 == size m2.

mul :: (Enum i, Num i, Ix i) => 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).

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

diagonal m extracts the diagonal of m.

Precondition: square m.

Modifying matrices
addRow :: (Ix i, Integral i) => 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 :: (Ix i, Num i, Enum i) => 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
tests :: IO BoolSource
Produced by Haddock version 2.6.0