| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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.
Instances

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

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

data Size i | Source

Size of a matrix.
Constructors

Size |

rows :: i |
cols :: i |

Instances

Eq i => Eq (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 | Source

data MIx i | Source

Type of matrix indices (row, column).
Constructors

MIx |

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

No nonpositive indices are allowed.
Generating and creating matrices

fromLists :: (Num i, Ix i) => Size i -> [[b]] -> Matrix i b | Source

``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 b | Source

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 c | Source

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

Generates a matrix of the given size.

matrixUsingRowGen | Source

:: (Arbitrary i, Integral i, Ix i, Arbitrary 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 :: Ix i => Matrix i b -> Size i | Source

The size of a matrix.

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

`True` iff the matrix is square.

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

Returns `True` iff the matrix is empty.

add :: (Ix i, Num i) => (a -> b -> c) -> Matrix i a -> Matrix i b -> Matrix i c | Source

``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 a | Source

``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 b | Source

``diagonal` m` extracts the diagonal of `m`. Precondition: ``square` m`.
Modifying matrices

addRow :: (Ix i, Integral i) => b -> Matrix i b -> Matrix i b | Source

``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 b | Source

``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 | Source

Produced by Haddock version 2.4.2