MiniAgda
Safe HaskellNone
LanguageHaskell98

SparseMatrix

Description

Sparse matrices. Original: Agda.Termination.SparseMatrix

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

Synopsis

Basic data types

data Matrix i b Source #

Type of matrices, parameterised on the type of values.

Constructors

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

Instances

Instances details
Functor (Matrix i) Source # 
Instance details

Defined in SparseMatrix

Methods

fmap :: (a -> b) -> Matrix i a -> Matrix i b #

(<$) :: a -> Matrix i b -> Matrix i a #

(Ord i, Integral i, Enum i, Show i, Show b, HasZero b) => Show (Matrix i b) Source # 
Instance details

Defined in SparseMatrix

Methods

showsPrec :: Int -> Matrix i b -> ShowS #

show :: Matrix i b -> String #

showList :: [Matrix i b] -> ShowS #

(Ord i, Eq a, HasZero a) => Eq (Matrix i a) Source # 
Instance details

Defined in SparseMatrix

Methods

(==) :: Matrix i a -> Matrix i a -> Bool #

(/=) :: Matrix i a -> Matrix i a -> Bool #

(HasZero b, Ord i, Ord b) => Ord (Matrix i b) Source # 
Instance details

Defined in 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 #

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

data Size i Source #

Size of a matrix.

Constructors

Size 

Fields

Instances

Instances details
Show i => Show (Size i) Source # 
Instance details

Defined in SparseMatrix

Methods

showsPrec :: Int -> Size i -> ShowS #

show :: Size i -> String #

showList :: [Size i] -> ShowS #

Eq i => Eq (Size i) Source # 
Instance details

Defined in SparseMatrix

Methods

(==) :: Size i -> Size i -> Bool #

(/=) :: Size i -> Size i -> Bool #

Ord i => Ord (Size i) Source # 
Instance details

Defined in 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 #

sizeInvariant :: (Ord i, Num i) => Size i -> Bool Source #

data MIx i Source #

Type of matrix indices (row, column).

Constructors

MIx 

Fields

Instances

Instances details
Ix i => Ix (MIx i) Source # 
Instance details

Defined in 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 #

Show i => Show (MIx i) Source # 
Instance details

Defined in SparseMatrix

Methods

showsPrec :: Int -> MIx i -> ShowS #

show :: MIx i -> String #

showList :: [MIx i] -> ShowS #

Eq i => Eq (MIx i) Source # 
Instance details

Defined in SparseMatrix

Methods

(==) :: MIx i -> MIx i -> Bool #

(/=) :: MIx i -> MIx i -> Bool #

Ord i => Ord (MIx i) Source # 
Instance details

Defined in 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 #

mIxInvariant :: (Ord i, Num i) => MIx i -> Bool Source #

No nonpositive indices are allowed.

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

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

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

Generates a matrix of the given size, using the given generator to generate the rows.

Generates a matrix of the given size.

Constructs a matrix from a list of (index, value)-pairs.

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

Converts a matrix to a list of row lists.

Combining and querying matrices

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

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 :: (Num i, Ix i, HasZero b) => Matrix i b -> Maybe b Source #

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

all :: (a -> Bool) -> Matrix i a -> Bool Source #

any :: (a -> Bool) -> Matrix i a -> Bool Source #

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

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

intersectWith f m1 m2 build the pointwise conjunction m1 and m2. Uses f to combine non-zero values.

Precondition: size m1 == size m2.

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

zip m1 m2 zips m1 and m2.

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

transpose :: Ord i => Matrix i b -> Matrix i b Source #

diagonal :: (Enum i, Num i, Ix i, Show i, HasZero b) => Matrix i b -> [b] Source #

diagonal m extracts the diagonal of m.

Precondition: square m.

Modifying matrices

addRow :: (Num i, HasZero b) => 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 :: (Num i, HasZero b) => 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