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

Safe HaskellNone

Agda.Termination.Matrix

Contents

Description

Naive implementation of simple matrix library.

Synopsis

Basic data types

data Matrix i b Source

Type of matrices, parameterised on the type of values.

Instances

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

data Size i Source

Size of a matrix.

Constructors

Size 

Fields

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

data MIx i Source

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

Arguments

:: (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 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 m1 m2 multiplies m1 and m2. Uses the operations of the 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