Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Termination.SparseMatrix

Contents

- Basic data types
- Generating and creating matrices
- Combining and querying matrices
- Modifying matrices
- Tests

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 {
  - 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 :: (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 :: (Show i, 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 :: (Show i, 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

data Matrix i b

Type of matrices, parameterised on the type of values.

Instances

Functor (Matrix i) |
(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