Safe Haskell	None
Language	Haskell2010

Agda.Termination.SparseMatrix

Contents

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

Description

Sparse matrices.

We assume the matrices to be very sparse, so we just implement them as sorted association lists.

Most operations are linear in the number of non-zero elements.

An exception is transposition, which needs to sort the association list again; it has the complexity of sorting: n log n where n is the number of non-zero elements.

Another exception is matrix multiplication, of course.

Synopsis

data Matrix i b = Matrix (Size i) [(MIx i, b)]
unM :: Matrix i b -> [(MIx i, b)]
data Size i = Size {
- rows :: i
- cols :: i
}
data MIx i = MIx {
- row :: i
- col :: i
}
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 :: (Integral i, HasZero b) => Matrix i b -> [[b]]
size :: Matrix i b -> Size i
square :: Ix i => Matrix i b -> Bool
isEmpty :: (Num i, Ix i) => Matrix i b -> Bool
isSingleton :: (Eq i, Num i, HasZero b) => Matrix i b -> Maybe b
zipMatrices :: forall a b c i. Ord i => (a -> c) -> (b -> c) -> (a -> b -> c) -> (c -> Bool) -> Matrix i a -> Matrix i b -> Matrix i c
add :: (Ord i, HasZero a) => (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
interAssocWith :: Ord i => (a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
mul :: (Ix i, Eq a) => Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
transpose :: Transpose a => a -> a
class Diagonal m e | m -> e where
toSparseRows :: Eq i => Matrix i b -> [(i, [(i, b)])]
supSize :: Ord i => Matrix i a -> Matrix i b -> Size i
zipAssocWith :: Ord i => ([(i, a)] -> [(i, c)]) -> ([(i, b)] -> [(i, c)]) -> (a -> Maybe c) -> (b -> Maybe c) -> (a -> b -> Maybe c) -> [(i, a)] -> [(i, b)] -> [(i, c)]
addRow :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b
addColumn :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b

Basic data types

data Matrix i b Source #

Type of matrices, parameterised on the type of values.

Sparse matrices are implemented as an ordered association list, mapping coordinates to values.

Constructors

Matrix (Size i) [(MIx i, b)]

Instances

Functor (Matrix i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods fmap :: (a -> b) -> Matrix i a -> Matrix i b # (<$) :: a -> Matrix i b -> Matrix i a #
Foldable (Matrix i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods fold :: Monoid m => Matrix i m -> m # foldMap :: Monoid m => (a -> m) -> Matrix i a -> m # foldr :: (a -> b -> b) -> b -> Matrix i a -> b # foldr' :: (a -> b -> b) -> b -> Matrix i a -> b # foldl :: (b -> a -> b) -> b -> Matrix i a -> b # foldl' :: (b -> a -> b) -> b -> Matrix i a -> b # foldr1 :: (a -> a -> a) -> Matrix i a -> a # foldl1 :: (a -> a -> a) -> Matrix i a -> a # toList :: Matrix i a -> [a] # null :: Matrix i a -> Bool # length :: Matrix i a -> Int # elem :: Eq a => a -> Matrix i a -> Bool # maximum :: Ord a => Matrix i a -> a # minimum :: Ord a => Matrix i a -> a # sum :: Num a => Matrix i a -> a # product :: Num a => Matrix i a -> a #
Traversable (Matrix i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods traverse :: Applicative f => (a -> f b) -> Matrix i a -> f (Matrix i b) # sequenceA :: Applicative f => Matrix i (f a) -> f (Matrix i a) # mapM :: Monad m => (a -> m b) -> Matrix i a -> m (Matrix i b) # sequence :: Monad m => Matrix i (m a) -> m (Matrix i a) #
(Eq i, Eq b) => Eq (Matrix i b) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods (==) :: Matrix i b -> Matrix i b -> Bool # (/=) :: Matrix i b -> Matrix i b -> Bool #
(Ord i, Ord b) => Ord (Matrix i b) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods compare :: Matrix i b -> Matrix i b -> Ordering # (<) :: Matrix i b -> Matrix i b -> Bool # (<=) :: Matrix i b -> Matrix i b -> Bool # (>) :: Matrix i b -> Matrix i b -> Bool # (>=) :: Matrix i b -> Matrix i b -> Bool # max :: Matrix i b -> Matrix i b -> Matrix i b # min :: Matrix i b -> Matrix i b -> Matrix i b #
(Integral i, HasZero b, Show i, Show b) => Show (Matrix i b) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods showsPrec :: Int -> Matrix i b -> ShowS # show :: Matrix i b -> String # showList :: [Matrix i b] -> ShowS #
(Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source #	Pointwise comparison. Only matrices with the same dimension are comparable.
Instance details Defined in Agda.Termination.SparseMatrix Methods comparable :: Comparable (Matrix i a) Source #
(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods pretty :: Matrix i b -> Doc Source # prettyPrec :: Int -> Matrix i b -> Doc Source # prettyList :: [Matrix i b] -> Doc Source #
(Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o) Source #	We assume the matrices have the same dimension.
Instance details Defined in Agda.Termination.Order Methods notWorse :: Matrix i o -> Matrix i o -> Bool Source #
(Integral i, HasZero b) => Diagonal (Matrix i b) b Source #	Diagonal of sparse matrix. `O(n)` where `n` is the number of non-zero elements in the matrix.
Instance details Defined in Agda.Termination.SparseMatrix Methods diagonal :: Matrix i b -> [b] Source #

unM :: Matrix i b -> [(MIx i, b)] Source #

Association of indices to values.

data Size i Source #

Size of a matrix.

Constructors

Size
Fields rows :: i Number of rows, `>= 0`. cols :: i Number of columns, `>= 0`.

Instances

Eq i => Eq (Size i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods (==) :: Size i -> Size i -> Bool # (/=) :: Size i -> Size i -> Bool #
Ord i => Ord (Size i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods compare :: Size i -> Size i -> Ordering # (<) :: Size i -> Size i -> Bool # (<=) :: Size i -> Size i -> Bool # (>) :: Size i -> Size i -> Bool # (>=) :: Size i -> Size i -> Bool # max :: Size i -> Size i -> Size i # min :: Size i -> Size i -> Size i #
Show i => Show (Size i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods showsPrec :: Int -> Size i -> ShowS # show :: Size i -> String # showList :: [Size i] -> ShowS #

data MIx i Source #

Type of matrix indices (row, column).

Constructors

MIx
Fields row :: i Row index, `1 <= row <= rows`. col :: i Column index `1 <= col <= cols`.

Instances

Eq i => Eq (MIx i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods (==) :: MIx i -> MIx i -> Bool # (/=) :: MIx i -> MIx i -> Bool #
Ord i => Ord (MIx i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods compare :: MIx i -> MIx i -> Ordering # (<) :: MIx i -> MIx i -> Bool # (<=) :: MIx i -> MIx i -> Bool # (>) :: MIx i -> MIx i -> Bool # (>=) :: MIx i -> MIx i -> Bool # max :: MIx i -> MIx i -> MIx i # min :: MIx i -> MIx i -> MIx i #
Show i => Show (MIx i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods showsPrec :: Int -> MIx i -> ShowS # show :: MIx i -> String # showList :: [MIx i] -> ShowS #
Ix i => Ix (MIx i) Source #
Instance details Defined in Agda.Termination.SparseMatrix Methods range :: (MIx i, MIx i) -> [MIx i] # index :: (MIx i, MIx i) -> MIx i -> Int # unsafeIndex :: (MIx i, MIx i) -> MIx i -> Int inRange :: (MIx i, MIx i) -> MIx i -> Bool # rangeSize :: (MIx i, MIx i) -> Int # unsafeRangeSize :: (MIx i, MIx i) -> Int

Generating and creating matrices

fromLists :: (Ord i, Num i, Enum i, HasZero b) => Size i -> [[b]] -> Matrix i b Source #

fromLists sz rs constructs a matrix from a list of lists of values (a list of rows). O(size) where size = rows × cols.

Precondition: length rs == rows sz and all ((cols sz ==) . length) rs.

fromIndexList :: (Ord i, HasZero b) => Size i -> [(MIx i, b)] -> Matrix i b Source #

Constructs a matrix from a list of (index, value)-pairs. O(n) where n is size of the list.

Precondition: indices are unique.

toLists :: (Integral i, HasZero b) => Matrix i b -> [[b]] Source #

Converts a matrix to a list of row lists. O(size) where size = rows × cols.

Combining and querying matrices

size :: Matrix i b -> Size i Source #

Dimensions of the 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.

isSingleton :: (Eq i, Num i, HasZero b) => Matrix i b -> Maybe b Source #

Returns 'Just b' iff it is a 1x1 matrix with just one entry b. O(1).

zipMatrices Source #

Arguments

:: Ord i
=> (a -> c)	Element only present in left matrix.
-> (b -> c)	Element only present in right matrix.
-> (a -> b -> c)	Element present in both matrices.
-> (c -> Bool)	Result counts as zero?
-> Matrix i a
-> Matrix i b
-> Matrix i c

General pointwise combination function for sparse matrices. O(n1 + n2).

add :: (Ord i, HasZero a) => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a Source #

add (+) m1 m2 adds m1 and m2, using (+) to add values. O(n1 + n2).

Returns a matrix of size supSize m1 m2.

intersectWith :: Ord i => (a -> a -> a) -> Matrix i a ->