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

 -}

module Agda.Termination.SparseMatrix
  ( -- * Basic data types
    Matrix(Matrix)
  , unM
  -- , matrixInvariant  -- Moved to the internal test-suite
  , Size(..)
  , MIx (..)
    -- * Generating and creating matrices
  , fromLists
  , fromIndexList
  , toLists
--  , Agda.Termination.Matrix.zipWith
  -- , matrix  -- Moved to the internal test-suite
    -- * Combining and querying matrices
  , size
  , square
  , isEmpty
  , isSingleton
  , zipMatrices
  , add
  , intersectWith
  , interAssocWith
  , mul
  , transpose
  , Diagonal(..)
  , toSparseRows
  , supSize
  , zipAssocWith
    -- * Modifying matrices
  , addRow
  , addColumn
  ) where

import Data.Array
import Data.Function
import qualified Data.List as List
import Data.Maybe


import qualified Data.Foldable as Fold

import qualified Text.PrettyPrint.Boxes as Boxes

import Agda.Termination.Semiring (HasZero(..), Semiring)
import qualified Agda.Termination.Semiring as Semiring


import Agda.Utils.List
import Agda.Utils.Maybe

import Agda.Utils.PartialOrd
import Agda.Utils.Pretty hiding (isEmpty)
import Agda.Utils.Tuple

import Agda.Utils.Impossible

------------------------------------------------------------------------
-- * Basic data types
------------------------------------------------------------------------

-- | Size of a matrix.

data Size i = Size
  { forall i. Size i -> i
rows :: i  -- ^ Number of rows,    @>= 0@.
  , forall i. Size i -> i
cols :: i  -- ^ Number of columns, @>= 0@.
  }
  deriving (Size i -> Size i -> Bool
forall i. Eq i => Size i -> Size i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Size i -> Size i -> Bool
$c/= :: forall i. Eq i => Size i -> Size i -> Bool
== :: Size i -> Size i -> Bool
$c== :: forall i. Eq i => Size i -> Size i -> Bool
Eq, Size i -> Size i -> Bool
Size i -> Size i -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {i}. Ord i => Eq (Size i)
forall i. Ord i => Size i -> Size i -> Bool
forall i. Ord i => Size i -> Size i -> Ordering
forall i. Ord i => Size i -> Size i -> Size i
min :: Size i -> Size i -> Size i
$cmin :: forall i. Ord i => Size i -> Size i -> Size i
max :: Size i -> Size i -> Size i
$cmax :: forall i. Ord i => Size i -> Size i -> Size i
>= :: Size i -> Size i -> Bool
$c>= :: forall i. Ord i => Size i -> Size i -> Bool
> :: Size i -> Size i -> Bool
$c> :: forall i. Ord i => Size i -> Size i -> Bool
<= :: Size i -> Size i -> Bool
$c<= :: forall i. Ord i => Size i -> Size i -> Bool
< :: Size i -> Size i -> Bool
$c< :: forall i. Ord i => Size i -> Size i -> Bool
compare :: Size i -> Size i -> Ordering
$ccompare :: forall i. Ord i => Size i -> Size i -> Ordering
Ord, Int -> Size i -> ShowS
forall i. Show i => Int -> Size i -> ShowS
forall i. Show i => [Size i] -> ShowS
forall i. Show i => Size i -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Size i] -> ShowS
$cshowList :: forall i. Show i => [Size i] -> ShowS
show :: Size i -> String
$cshow :: forall i. Show i => Size i -> String
showsPrec :: Int -> Size i -> ShowS
$cshowsPrec :: forall i. Show i => Int -> Size i -> ShowS
Show)

-- | Type of matrix indices (row, column).

data MIx i = MIx
  { forall i. MIx i -> i
row :: i  -- ^ Row index,   @1 <= row <= rows@.
  , forall i. MIx i -> i
col :: i  -- ^ Column index @1 <= col <= cols@.
  }
  deriving (MIx i -> MIx i -> Bool
forall i. Eq i => MIx i -> MIx i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MIx i -> MIx i -> Bool
$c/= :: forall i. Eq i => MIx i -> MIx i -> Bool
== :: MIx i -> MIx i -> Bool
$c== :: forall i. Eq i => MIx i -> MIx i -> Bool
Eq, MIx i -> MIx i -> Bool
MIx i -> MIx i -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {i}. Ord i => Eq (MIx i)
forall i. Ord i => MIx i -> MIx i -> Bool
forall i. Ord i => MIx i -> MIx i -> Ordering
forall i. Ord i => MIx i -> MIx i -> MIx i
min :: MIx i -> MIx i -> MIx i
$cmin :: forall i. Ord i => MIx i -> MIx i -> MIx i
max :: MIx i -> MIx i -> MIx i
$cmax :: forall i. Ord i => MIx i -> MIx i -> MIx i
>= :: MIx i -> MIx i -> Bool
$c>= :: forall i. Ord i => MIx i -> MIx i -> Bool
> :: MIx i -> MIx i -> Bool
$c> :: forall i. Ord i => MIx i -> MIx i -> Bool
<= :: MIx i -> MIx i -> Bool
$c<= :: forall i. Ord i => MIx i -> MIx i -> Bool
< :: MIx i -> MIx i -> Bool
$c< :: forall i. Ord i => MIx i -> MIx i -> Bool
compare :: MIx i -> MIx i -> Ordering
$ccompare :: forall i. Ord i => MIx i -> MIx i -> Ordering
Ord, Int -> MIx i -> ShowS
forall i. Show i => Int -> MIx i -> ShowS
forall i. Show i => [MIx i] -> ShowS
forall i. Show i => MIx i -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MIx i] -> ShowS
$cshowList :: forall i. Show i => [MIx i] -> ShowS
show :: MIx i -> String
$cshow :: forall i. Show i => MIx i -> String
showsPrec :: Int -> MIx i -> ShowS
$cshowsPrec :: forall i. Show i => Int -> MIx i -> ShowS
Show, (MIx i, MIx i) -> [MIx i]
(MIx i, MIx i) -> MIx i -> Bool
(MIx i, MIx i) -> MIx i -> Int
forall a.
Ord a
-> ((a, a) -> [a])
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Bool)
-> ((a, a) -> Int)
-> ((a, a) -> Int)
-> Ix a
forall {i}. Ix i => Ord (MIx i)
forall i. Ix i => (MIx i, MIx i) -> Int
forall i. Ix i => (MIx i, MIx i) -> [MIx i]
forall i. Ix i => (MIx i, MIx i) -> MIx i -> Bool
forall i. Ix i => (MIx i, MIx i) -> MIx i -> Int
unsafeRangeSize :: (MIx i, MIx i) -> Int
$cunsafeRangeSize :: forall i. Ix i => (MIx i, MIx i) -> Int
rangeSize :: (MIx i, MIx i) -> Int
$crangeSize :: forall i. Ix i => (MIx i, MIx i) -> Int
inRange :: (MIx i, MIx i) -> MIx i -> Bool
$cinRange :: forall i. Ix i => (MIx i, MIx i) -> MIx i -> Bool
unsafeIndex :: (MIx i, MIx i) -> MIx i -> Int
$cunsafeIndex :: forall i. Ix i => (MIx i, MIx i) -> MIx i -> Int
index :: (MIx i, MIx i) -> MIx i -> Int
$cindex :: forall i. Ix i => (MIx i, MIx i) -> MIx i -> Int
range :: (MIx i, MIx i) -> [MIx i]
$crange :: forall i. Ix i => (MIx i, MIx i) -> [MIx i]
Ix)

-- UNUSED Liang-Ting Chen 2019-07-15
---- | Convert a 'Size' to a set of bounds suitable for use with
----   the matrices in this module.
--
--toBounds :: Num i => Size i -> (MIx i, MIx i)
--toBounds sz = (MIx { row = 1, col = 1 }, MIx { row = rows sz, col = cols sz })

-- | Type of matrices, parameterised on the type of values.
--
--   Sparse matrices are implemented as an ordered association list,
--   mapping coordinates to values.

data Matrix i b = Matrix
  { forall i b. Matrix i b -> Size i
size :: Size i        -- ^ Dimensions of the matrix.
  , forall i b. Matrix i b -> [(MIx i, b)]
unM  :: [(MIx i, b)]  -- ^ Association of indices to values.
  }
  deriving (Matrix i b -> Matrix i b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i b. (Eq i, Eq b) => Matrix i b -> Matrix i b -> Bool
/= :: Matrix i b -> Matrix i b -> Bool
$c/= :: forall i b. (Eq i, Eq b) => Matrix i b -> Matrix i b -> Bool
== :: Matrix i b -> Matrix i b -> Bool
$c== :: forall i b. (Eq i, Eq b) => Matrix i b -> Matrix i b -> Bool
Eq, Matrix i b -> Matrix i b -> Bool
Matrix i b -> Matrix i b -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {i} {b}. (Ord i, Ord b) => Eq (Matrix i b)
forall i b. (Ord i, Ord b) => Matrix i b -> Matrix i b -> Bool
forall i b. (Ord i, Ord b) => Matrix i b -> Matrix i b -> Ordering
forall i b.
(Ord i, Ord b) =>
Matrix i b -> Matrix i b -> Matrix i b
min :: Matrix i b -> Matrix i b -> Matrix i b
$cmin :: forall i b.
(Ord i, Ord b) =>
Matrix i b -> Matrix i b -> Matrix i b
max :: Matrix i b -> Matrix i b -> Matrix i b
$cmax :: forall i b.
(Ord i, Ord b) =>
Matrix i b -> Matrix i b -> Matrix i b
>= :: Matrix i b -> Matrix i b -> Bool
$c>= :: forall i b. (Ord i, Ord b) => Matrix i b -> Matrix i b -> Bool
> :: Matrix i b -> Matrix i b -> Bool
$c> :: forall i b. (Ord i, Ord b) => Matrix i b -> Matrix i b -> Bool
<= :: Matrix i b -> Matrix i b -> Bool
$c<= :: forall i b. (Ord i, Ord b) => Matrix i b -> Matrix i b -> Bool
< :: Matrix i b -> Matrix i b -> Bool
$c< :: forall i b. (Ord i, Ord b) => Matrix i b -> Matrix i b -> Bool
compare :: Matrix i b -> Matrix i b -> Ordering
$ccompare :: forall i b. (Ord i, Ord b) => Matrix i b -> Matrix i b -> Ordering
Ord, forall a b. a -> Matrix i b -> Matrix i a
forall a b. (a -> b) -> Matrix i a -> Matrix i b
forall i a b. a -> Matrix i b -> Matrix i a
forall i a b. (a -> b) -> Matrix i a -> Matrix i b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Matrix i b -> Matrix i a
$c<$ :: forall i a b. a -> Matrix i b -> Matrix i a
fmap :: forall a b. (a -> b) -> Matrix i a -> Matrix i b
$cfmap :: forall i a b. (a -> b) -> Matrix i a -> Matrix i b
Functor, forall a. Matrix i a -> Bool
forall i a. Eq a => a -> Matrix i a -> Bool
forall i a. Num a => Matrix i a -> a
forall i a. Ord a => Matrix i a -> a
forall m a. Monoid m => (a -> m) -> Matrix i a -> m
forall i m. Monoid m => Matrix i m -> m
forall i a. Matrix i a -> Bool
forall i a. Matrix i a -> Int
forall i a. Matrix i a -> [a]
forall a b. (a -> b -> b) -> b -> Matrix i a -> b
forall i a. (a -> a -> a) -> Matrix i a -> a
forall i m a. Monoid m => (a -> m) -> Matrix i a -> m
forall i b a. (b -> a -> b) -> b -> Matrix i a -> b
forall i a b. (a -> b -> b) -> b -> Matrix i a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Matrix i a -> a
$cproduct :: forall i a. Num a => Matrix i a -> a
sum :: forall a. Num a => Matrix i a -> a
$csum :: forall i a. Num a => Matrix i a -> a
minimum :: forall a. Ord a => Matrix i a -> a
$cminimum :: forall i a. Ord a => Matrix i a -> a
maximum :: forall a. Ord a => Matrix i a -> a
$cmaximum :: forall i a. Ord a => Matrix i a -> a
elem :: forall a. Eq a => a -> Matrix i a -> Bool
$celem :: forall i a. Eq a => a -> Matrix i a -> Bool
length :: forall a. Matrix i a -> Int
$clength :: forall i a. Matrix i a -> Int
null :: forall a. Matrix i a -> Bool
$cnull :: forall i a. Matrix i a -> Bool
toList :: forall a. Matrix i a -> [a]
$ctoList :: forall i a. Matrix i a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Matrix i a -> a
$cfoldl1 :: forall i a. (a -> a -> a) -> Matrix i a -> a
foldr1 :: forall a. (a -> a -> a) -> Matrix i a -> a
$cfoldr1 :: forall i a. (a -> a -> a) -> Matrix i a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Matrix i a -> b
$cfoldl' :: forall i b a. (b -> a -> b) -> b -> Matrix i a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Matrix i a -> b
$cfoldl :: forall i b a. (b -> a -> b) -> b -> Matrix i a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Matrix i a -> b
$cfoldr' :: forall i a b. (a -> b -> b) -> b -> Matrix i a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Matrix i a -> b
$cfoldr :: forall i a b. (a -> b -> b) -> b -> Matrix i a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Matrix i a -> m
$cfoldMap' :: forall i m a. Monoid m => (a -> m) -> Matrix i a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Matrix i a -> m
$cfoldMap :: forall i m a. Monoid m => (a -> m) -> Matrix i a -> m
fold :: forall m. Monoid m => Matrix i m -> m
$cfold :: forall i m. Monoid m => Matrix i m -> m
Foldable, forall i. Functor (Matrix i)
forall i. Foldable (Matrix i)
forall i (m :: * -> *) a.
Monad m =>
Matrix i (m a) -> m (Matrix i a)
forall i (f :: * -> *) a.
Applicative f =>
Matrix i (f a) -> f (Matrix i a)
forall i (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Matrix i a -> m (Matrix i b)
forall i (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Matrix i a -> f (Matrix i b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Matrix i a -> f (Matrix i b)
sequence :: forall (m :: * -> *) a. Monad m => Matrix i (m a) -> m (Matrix i a)
$csequence :: forall i (m :: * -> *) a.
Monad m =>
Matrix i (m a) -> m (Matrix i a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Matrix i a -> m (Matrix i b)
$cmapM :: forall i (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Matrix i a -> m (Matrix i b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Matrix i (f a) -> f (Matrix i a)
$csequenceA :: forall i (f :: * -> *) a.
Applicative f =>
Matrix i (f a) -> f (Matrix i a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Matrix i a -> f (Matrix i b)
$ctraverse :: forall i (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Matrix i a -> f (Matrix i b)
Traversable)

------------------------------------------------------------------------
-- * Operations and query on matrix size.
------------------------------------------------------------------------

-- | 'True' iff the matrix is square.

square :: Ix i => Matrix i b -> Bool
square :: forall i b. Ix i => Matrix i b -> Bool
square Matrix i b
m = forall i. Size i -> i
rows (forall i b. Matrix i b -> Size i
size Matrix i b
m) forall a. Eq a => a -> a -> Bool
== forall i. Size i -> i
cols (forall i b. Matrix i b -> Size i
size Matrix i b
m)

-- | Returns 'True' iff the matrix is empty.

isEmpty :: (Num i, Ix i) => Matrix i b -> Bool
isEmpty :: forall i b. (Num i, Ix i) => Matrix i b -> Bool
isEmpty Matrix i b
m = forall i. Size i -> i
rows Size i
sz forall a. Ord a => a -> a -> Bool
<= i
0 Bool -> Bool -> Bool
|| forall i. Size i -> i
cols Size i
sz forall a. Ord a => a -> a -> Bool
<= i
0
  where sz :: Size i
sz = forall i b. Matrix i b -> Size i
size Matrix i b
m

-- | Compute the matrix size of the union of two matrices.

supSize :: Ord i => Matrix i a -> Matrix i b -> Size i
supSize :: forall i a b. Ord i => Matrix i a -> Matrix i b -> Size i
supSize (Matrix (Size i
r1 i
c1) [(MIx i, a)]
_) (Matrix (Size i
r2 i
c2) [(MIx i, b)]
_) =
  forall i. i -> i -> Size i
Size (forall a. Ord a => a -> a -> a
max i
r1 i
r2) (forall a. Ord a => a -> a -> a
max i
c1 i
c2)

-- | Compute the matrix size of the intersection of two matrices.

infSize :: Ord i => Matrix i a -> Matrix i b -> Size i
infSize :: forall i a b. Ord i => Matrix i a -> Matrix i b -> Size i
infSize (Matrix (Size i
r1 i
c1) [(MIx i, a)]
_) (Matrix (Size i
r2 i
c2) [(MIx i, b)]
_) =
  forall i. i -> i -> Size i
Size (forall a. Ord a => a -> a -> a
min i
r1 i
r2) (forall a. Ord a => a -> a -> a
min i
c1 i
c2)

------------------------------------------------------------------------
-- * Creating matrices and converting to lists.
------------------------------------------------------------------------

-- | Constructs a matrix from a list of @(index, value)@-pairs.
--   @O(n)@ where @n@ is size of the list.
--
--   Precondition: indices are unique.

fromIndexList :: (Ord i, HasZero b) => Size i -> [(MIx i, b)] -> Matrix i b
fromIndexList :: forall i b.
(Ord i, HasZero b) =>
Size i -> [(MIx i, b)] -> Matrix i b
fromIndexList Size i
sz = forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix Size i
sz
                 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)
                 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. HasZero a => a
zeroElement forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)

-- | @'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@.

fromLists :: (Ord i, Num i, Enum i, HasZero b) => Size i -> [[b]] -> Matrix i b
fromLists :: forall i b.
(Ord i, Num i, Enum i, HasZero b) =>
Size i -> [[b]] -> Matrix i b
fromLists Size i
sz [[b]]
bs = forall i b.
(Ord i, HasZero b) =>
Size i -> [(MIx i, b)] -> Matrix i b
fromIndexList Size i
sz forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip ([ forall i. i -> i -> MIx i
MIx i
i i
j | i
i <- [i
1..forall i. Size i -> i
rows Size i
sz]
                                                    , i
j <- [i
1..forall i. Size i -> i
cols Size i
sz]]) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[b]]
bs)

-- | Converts a sparse matrix to a sparse list of rows.
--   @O(n)@ where @n@ is the number of non-zero entries of the matrix.
--
--   Only non-empty rows are generated.
--

toSparseRows :: (Eq i) => Matrix i b -> [(i,[(i,b)])]
toSparseRows :: forall i b. Eq i => Matrix i b -> [(i, [(i, b)])]
toSparseRows (Matrix Size i
_ []) = []
toSparseRows (Matrix Size i
_ ((MIx i
i i
j, b
b) : [(MIx i, b)]
m)) = forall {a} {b}.
Eq a =>
a -> [(a, b)] -> [(MIx a, b)] -> [(a, [(a, b)])]
aux i
i [(i
j,b
b)] [(MIx i, b)]
m
  where aux :: a -> [(a, b)] -> [(MIx a, b)] -> [(a, [(a, b)])]
aux a
i' []  [] = []
        aux a
i' [(a, b)]
row [] = [(a
i', forall a. [a] -> [a]
reverse [(a, b)]
row)]
        aux a
i' [(a, b)]
row ((MIx a
i a
j, b
b) : [(MIx a, b)]
m)
          | a
i' forall a. Eq a => a -> a -> Bool
== a
i   = a -> [(a, b)] -> [(MIx a, b)] -> [(a, [(a, b)])]
aux a
i' ((a
j,b
b)forall a. a -> [a] -> [a]
:[(a, b)]
row) [(MIx a, b)]
m
          | Bool
otherwise = (a
i', forall a. [a] -> [a]
reverse [(a, b)]
row) forall a. a -> [a] -> [a]
: a -> [(a, b)] -> [(MIx a, b)] -> [(a, [(a, b)])]
aux a
i [(a
j,b
b)] [(MIx a, b)]
m

-- | Turn a sparse vector into a vector by inserting a fixed element
--   at the missing positions.
--   @O(size)@ where @size@ is the dimension of the vector.

blowUpSparseVec :: (Integral i) => b -> i -> [(i,b)] -> [b]
blowUpSparseVec :: forall i b. Integral i => b -> i -> [(i, b)] -> [b]
blowUpSparseVec b
zero i
n [(i, b)]
l = i -> [(i, b)] -> [b]
aux i
1 [(i, b)]
l
  where aux :: i -> [(i, b)] -> [b]
aux i
i []           = forall i a. Integral i => i -> a -> [a]
List.genericReplicate (i
n forall a. Num a => a -> a -> a
+ i
1 forall a. Num a => a -> a -> a
- i
i) b
zero
        aux i
i l :: [(i, b)]
l@((i
j,b
b):[(i, b)]
l')
          | i
i forall a. Ord a => a -> a -> Bool
> i
j Bool -> Bool -> Bool
|| i
i forall a. Ord a => a -> a -> Bool
> i
n = forall a. HasCallStack => a
__IMPOSSIBLE__
          | i
i forall a. Eq a => a -> a -> Bool
== i
j         = b
b    forall a. a -> [a] -> [a]
: i -> [(i, b)] -> [b]
aux (i
i forall a. Num a => a -> a -> a
+ i
1) [(i, b)]
l'
          | Bool
otherwise      = b
zero forall a. a -> [a] -> [a]
: i -> [(i, b)] -> [b]
aux (i
i forall a. Num a => a -> a -> a
+ i
1) [(i, b)]
l

-- UNUSED Liang-Ting Chen 2019-07-15
---- Older implementation without replicate.
--blowUpSparseVec' :: (Ord i, Num i, Enum i) => b -> i -> [(i,b)] -> [b]
--blowUpSparseVec' zero n l = aux 1 l
--  where aux i [] | i > n = []
--                 | otherwise = zero : aux (i+1) []
--        aux i ((j,b):l) | i <= n && j == i = b : aux (succ i) l
--        aux i ((j,b):l) | i <= n && j >= i = zero : aux (succ i) ((j,b):l)
--        aux i l = __IMPOSSIBLE__
--          -- error $ "blowUpSparseVec (n = " ++ show n ++ ") aux i=" ++ show i ++ " j=" ++ show (fst (head l)) ++ " length l = " ++ show (length l)
--
-- | Converts a matrix to a list of row lists.
--   @O(size)@ where @size = rows × cols@.

toLists :: (Integral i, HasZero b) => Matrix i b -> [[b]]
toLists :: forall i b. (Integral i, HasZero b) => Matrix i b -> [[b]]
toLists m :: Matrix i b
m@(Matrix size :: Size i
size@(Size i
nrows i
ncols) [(MIx i, b)]
_) =
    forall i b. Integral i => b -> i -> [(i, b)] -> [b]
blowUpSparseVec [b]
emptyRow i
nrows forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map (forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (forall i b. Integral i => b -> i -> [(i, b)] -> [b]
blowUpSparseVec forall a. HasZero a => a
zeroElement i
ncols)) forall a b. (a -> b) -> a -> b
$ forall i b. Eq i => Matrix i b -> [(i, [(i, b)])]
toSparseRows Matrix i b
m
  where
    emptyRow :: [b]
emptyRow = forall i a. Integral i => i -> a -> [a]
List.genericReplicate i
ncols forall a. HasZero a => a
zeroElement

------------------------------------------------------------------------
-- * Combining and querying matrices
------------------------------------------------------------------------

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

isSingleton :: (Eq i, Num i, HasZero b) => Matrix i b -> Maybe b
isSingleton :: forall i b. (Eq i, Num i, HasZero b) => Matrix i b -> Maybe b
isSingleton (Matrix (Size i
1 i
1) [(MIx i
_,b
b)]) = forall a. a -> Maybe a
Just b
b
isSingleton (Matrix (Size i
1 i
1) []     ) = forall a. a -> Maybe a
Just forall a. HasZero a => a
zeroElement
isSingleton (Matrix (Size i
1 i
1) [(MIx i, b)]
_      ) = forall a. HasCallStack => a
__IMPOSSIBLE__
isSingleton Matrix i b
_ = forall a. Maybe a
Nothing

-- | @'diagonal' m@ extracts the diagonal of @m@.
--
--   For non-square matrices, the length of the diagonal is
--   the minimum of the dimensions of the matrix.

class Diagonal m e | m -> e where
  diagonal :: m -> [e]

-- | Diagonal of sparse matrix.
--
--   @O(n)@ where @n@ is the number of non-zero elements in the matrix.

instance (Integral i, HasZero b) => Diagonal (Matrix i b) b where
  diagonal :: Matrix i b -> [b]
diagonal (Matrix (Size i
r i
c) [(MIx i, b)]
m) =
    forall i b. Integral i => b -> i -> [(i, b)] -> [b]
blowUpSparseVec forall a. HasZero a => a
zeroElement (forall a. Ord a => a -> a -> a
min i
r i
c) forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ ((MIx i
i i
j), b
b) -> if i
iforall a. Eq a => a -> a -> Bool
==i
j then forall a. a -> Maybe a
Just (i
i,b
b) else forall a. Maybe a
Nothing) [(MIx i, b)]
m

-- | Transposable things.

class Transpose a where
  transpose :: a -> a

-- | Size of transposed matrix.

instance Transpose (Size i) where
  transpose :: Size i -> Size i
transpose (Size i
n i
m) = forall i. i -> i -> Size i
Size i
m i
n

-- | Transposing coordinates.

instance Transpose (MIx i) where
  transpose :: MIx i -> MIx i
transpose (MIx i
i i
j) = forall i. i -> i -> MIx i
MIx i
j i
i

-- | Matrix transposition.
--
--   @O(n log n)@ where @n@ is the number of non-zero elements in the matrix.

instance Ord i => Transpose (Matrix i b) where
  transpose :: Matrix i b -> Matrix i b
transpose (Matrix Size i
size [(MIx i, b)]
m) =
    forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix (forall a. Transpose a => a -> a
transpose Size i
size) forall a b. (a -> b) -> a -> b
$
      forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$
        forall a b. (a -> b) -> [a] -> [b]
map (forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst forall a. Transpose a => a -> a
transpose) [(MIx i, b)]
m


-- | General pointwise combination function for association lists.
--   @O(n1 + n2)@ where @ni@ is the number of non-zero element in matrix @i@.
--
--   In @zipAssocWith fs gs f g h l l'@,
--
--   @fs@ is possibly more efficient version of
--   @'mapMaybe' (\ (i, a) -> (i,) <$> f a)@, and same for @gs@ and @g@.

zipAssocWith :: (Ord i)
  => ([(i,a)] -> [(i,c)]) -- ^ Only left map remaining.
  -> ([(i,b)] -> [(i,c)]) -- ^ Only right map remaining.
  -> (a -> Maybe c)       -- ^ Element only present in left map.
  -> (b -> Maybe c)       -- ^ Element only present in right map.
  -> (a -> b -> Maybe c)  -- ^ Element present in both maps.
  -> [(i,a)] -> [(i,b)] -> [(i,c)]
zipAssocWith :: forall i a c b.
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)]
zipAssocWith [(i, a)] -> [(i, c)]
fs [(i, b)] -> [(i, c)]
gs a -> Maybe c
f b -> Maybe c
g a -> b -> Maybe c
h = [(i, a)] -> [(i, b)] -> [(i, c)]
merge
  where
    merge :: [(i, a)] -> [(i, b)] -> [(i, c)]
merge [(i, a)]
m1 [] = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (i
i, a
a) -> (i
i,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe c
f a
a) [(i, a)]
m1
    merge [] [(i, b)]
m2 = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (i
i, b
b) -> (i
i,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> Maybe c
g b
b) [(i, b)]
m2
    merge m1 :: [(i, a)]
m1@((i
i,a
a):[(i, a)]
m1') m2 :: [(i, b)]
m2@((i
j,b
b):[(i, b)]
m2') =
      case forall a. Ord a => a -> a -> Ordering
compare i
i i
j of
        Ordering
LT -> forall a. Maybe a -> [a] -> [a]
mcons ((i
i,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe c
f a
a)   forall a b. (a -> b) -> a -> b
$ [(i, a)] -> [(i, b)] -> [(i, c)]
merge [(i, a)]
m1' [(i, b)]
m2
        Ordering
GT -> forall a. Maybe a -> [a] -> [a]
mcons ((i
j,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> Maybe c
g b
b)   forall a b. (a -> b) -> a -> b
$ [(i, a)] -> [(i, b)] -> [(i, c)]
merge [(i, a)]
m1  [(i, b)]
m2'
        Ordering
EQ -> forall a. Maybe a -> [a] -> [a]
mcons ((i
i,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> Maybe c
h a
a b
b) forall a b. (a -> b) -> a -> b
$ [(i, a)] -> [(i, b)] -> [(i, c)]
merge [(i, a)]
m1' [(i, b)]
m2'

-- | Instance of 'zipAssocWith' which keeps longer assoc lists.
--   @O(n1 + n2)@.

unionAssocWith  :: (Ord i)
  => (a -> Maybe c)       -- ^ Element only present in left map.
  -> (b -> Maybe c)       -- ^ Element only present in right map.
  -> (a -> b -> Maybe c)  -- ^ Element present in both maps.
  -> [(i,a)] -> [(i,b)] -> [(i,c)]
unionAssocWith :: forall i a c b.
Ord i =>
(a -> Maybe c)
-> (b -> Maybe c)
-> (a -> b -> Maybe c)
-> [(i, a)]
-> [(i, b)]
-> [(i, c)]
unionAssocWith a -> Maybe c
f b -> Maybe c
g a -> b -> Maybe c
h = forall i a c b.
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)]
zipAssocWith (forall {t} {a} {t}. (t -> Maybe a) -> [(t, t)] -> [(t, a)]
map_ a -> Maybe c
f) (forall {t} {a} {t}. (t -> Maybe a) -> [(t, t)] -> [(t, a)]
map_ b -> Maybe c
g) a -> Maybe c
f b -> Maybe c
g a -> b -> Maybe c
h
  where
    map_ :: (t -> Maybe a) -> [(t, t)] -> [(t, a)]
map_ t -> Maybe a
f = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (t
i, t
a) -> (t
i,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> Maybe a
f t
a)

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

zipMatrices :: forall a b c i . (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
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
zipMatrices a -> c
f b -> c
g a -> b -> c
h c -> Bool
zero Matrix i a
m1 Matrix i b
m2 = forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix (forall i a b. Ord i => Matrix i a -> Matrix i b -> Size i
supSize Matrix i a
m1 Matrix i b
m2) forall a b. (a -> b) -> a -> b
$
  forall i a c b.
Ord i =>
(a -> Maybe c)
-> (b -> Maybe c)
-> (a -> b -> Maybe c)
-> [(i, a)]
-> [(i, b)]
-> [(i, c)]
unionAssocWith (c -> Maybe c
drop0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> c
f) (c -> Maybe c
drop0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c
g) (\ a
a -> c -> Maybe c
drop0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c
h a
a) (forall i b. Matrix i b -> [(MIx i, b)]
unM Matrix i a
m1) (forall i b. Matrix i b -> [(MIx i, b)]
unM Matrix i b
m2)
  where
    drop0 :: c -> Maybe c
drop0 = forall a. (a -> Bool) -> a -> Maybe a
filterMaybe (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> Bool
zero)

-- | @'add' (+) m1 m2@ adds @m1@ and @m2@, using @(+)@ to add values.
--   @O(n1 + n2)@.
--
--   Returns a matrix of size @'supSize' m1 m2@.

add :: (Ord i, HasZero a) => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
add :: forall i a.
(Ord i, HasZero a) =>
(a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
add a -> a -> a
plus = 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
zipMatrices forall a. a -> a
id forall a. a -> a
id a -> a -> a
plus (forall a. Eq a => a -> a -> Bool
== forall a. HasZero a => a
zeroElement)

-- | @'intersectWith' f m1 m2@ build the pointwise conjunction @m1@ and @m2@.
--   Uses @f@ to combine non-zero values.
--   @O(n1 + n2)@.
--
--   Returns a matrix of size @infSize m1 m2@.

intersectWith :: (Ord i) => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
intersectWith :: forall i a.
Ord i =>
(a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
intersectWith a -> a -> a
f Matrix i a
m1 Matrix i a
m2 = forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix (forall i a b. Ord i => Matrix i a -> Matrix i b -> Size i
infSize Matrix i a
m1 Matrix i a
m2) forall a b. (a -> b) -> a -> b
$ forall i a.
Ord i =>
(a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
interAssocWith a -> a -> a
f (forall i b. Matrix i b -> [(MIx i, b)]
unM Matrix i a
m1) (forall i b. Matrix i b -> [(MIx i, b)]
unM Matrix i a
m2)

-- | Association list intersection.
--   @O(n1 + n2)@.
--
--   @interAssocWith f l l' = { (i, f a b) | (i,a) ∈ l and (i,b) ∈ l' }@
--
--   Used to combine sparse matrices, it might introduce zero elements
--   if @f@ can return zero for non-zero arguments.

interAssocWith :: (Ord i) => (a -> a -> a) -> [(i,a)] -> [(i,a)] -> [(i,a)]
interAssocWith :: forall i a.
Ord i =>
(a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
interAssocWith a -> a -> a
f [] [(i, a)]
m = []
interAssocWith a -> a -> a
f [(i, a)]
l [] = []
interAssocWith a -> a -> a
f l :: [(i, a)]
l@((i
i,a
a):[(i, a)]
l') m :: [(i, a)]
m@((i
j,a
b):[(i, a)]
m')
    | i
i forall a. Ord a => a -> a -> Bool
< i
j = forall i a.
Ord i =>
(a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
interAssocWith a -> a -> a
f [(i, a)]
l' [(i, a)]
m
    | i
i forall a. Ord a => a -> a -> Bool
> i
j = forall i a.
Ord i =>
(a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
interAssocWith a -> a -> a
f [(i, a)]
l [(i, a)]
m'
    | Bool
otherwise = (i
i, a -> a -> a
f a
a a
b) forall a. a -> [a] -> [a]
: forall i a.
Ord i =>
(a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
interAssocWith a -> a -> a
f [(i, a)]
l' [(i, a)]
m'

-- | @'mul' semiring m1 m2@ multiplies matrices @m1@ and @m2@.
--   Uses the operations of the semiring @semiring@ to perform the
--   multiplication.
--
--   @O(n1 + n2 log n2 + Σ(i <= r1) Σ(j <= c2) d(i,j))@ where
--   @r1@ is the number of non-empty rows in @m1@ and
--   @c2@ is the number of non-empty columns in @m2@ and
--   @d(i,j)@  is the bigger one of the following two quantifies:
--   the length of sparse row @i@ in @m1@ and
--   the length of sparse column @j@ in @m2@.
--
--   Given dimensions @m1 : r1 × c1@ and @m2 : r2 × c2@,
--   a matrix of size @r1 × c2@ is returned.
--   It is not necessary that @c1 == r2@, the matrices are implicitly
--   patched with zeros to match up for multiplication.
--   For sparse matrices, this patching is a no-op.

mul :: (Ix i, Eq a)
    => Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
mul :: forall i a.
(Ix i, Eq a) =>
Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
mul Semiring a
semiring Matrix i a
m1 Matrix i a
m2 = forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix (Size { rows :: i
rows = forall i. Size i -> i
rows (forall i b. Matrix i b -> Size i
size Matrix i a
m1), cols :: i
cols = forall i. Size i -> i
cols (forall i b. Matrix i b -> Size i
size Matrix i a
m2) }) forall a b. (a -> b) -> a -> b
$
  [ (forall i. i -> i -> MIx i
MIx i
i i
j, a
b)
    | (i
i,[(i, a)]
v) <- forall i b. Eq i => Matrix i b -> [(i, [(i, b)])]
toSparseRows Matrix i a
m1
    , (i
j,[(i, a)]
w) <- forall i b. Eq i => Matrix i b -> [(i, [(i, b)])]
toSparseRows forall a b. (a -> b) -> a -> b
$ forall a. Transpose a => a -> a
transpose Matrix i a
m2
    , let b :: a
b = [(i, a)] -> [(i, a)] -> a
inner [(i, a)]
v [(i, a)]
w
    , a
b forall a. Eq a => a -> a -> Bool
/= a
zero
  ]
  where
     zero :: a
zero  = forall a. Semiring a -> a
Semiring.zero Semiring a
semiring
     plus :: a -> a -> a
plus  = forall a. Semiring a -> a -> a -> a
Semiring.add  Semiring a
semiring
     times :: a -> a -> a
times = forall a. Semiring a -> a -> a -> a
Semiring.mul  Semiring a
semiring
     inner :: [(i, a)] -> [(i, a)] -> a
inner [(i, a)]
v [(i, a)]
w = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' a -> a -> a
plus a
zero forall a b. (a -> b) -> a -> b
$
                   forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall i a.
Ord i =>
(a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
interAssocWith a -> a -> a
times [(i, a)]
v [(i, a)]
w

-- | Pointwise comparison.
--   Only matrices with the same dimension are comparable.
instance (Ord i, PartialOrd a) => PartialOrd (Matrix i a) where
  comparable :: Comparable (Matrix i a)
comparable Matrix i a
m Matrix i a
n
    | forall i b. Matrix i b -> Size i
size Matrix i a
m forall a. Eq a => a -> a -> Bool
/= forall i b. Matrix i b -> Size i
size Matrix i a
n = PartialOrdering
POAny
    | Bool
otherwise        = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold forall a b. (a -> b) -> a -> b
$
                           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
zipMatrices forall {p}. p -> PartialOrdering
onlym forall {p}. p -> PartialOrdering
onlyn Comparable a
both PartialOrdering -> Bool
trivial Matrix i a
m Matrix i a
n
    where
      -- If an element is only in @m@, then its 'Unknown' in @n@
      -- so it gotten better at best, in any case, not worse.
      onlym :: p -> PartialOrdering
onlym p
o = PartialOrdering
POGT
      -- If an element is only in @n@, then its 'Unknown' in @m@
      -- so we have strictly less information.
      onlyn :: p -> PartialOrdering
onlyn p
o = PartialOrdering
POLT
      both :: Comparable a
both    = forall a. PartialOrd a => Comparable a
comparable
      -- The zero element of the result sparse matrix is the
      -- neutral element of the monoid.
      trivial :: PartialOrdering -> Bool
trivial = (forall a. Eq a => a -> a -> Bool
==forall a. Monoid a => a
mempty)

------------------------------------------------------------------------
-- Modifying matrices

-- | @'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@.

addColumn :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b
addColumn :: forall i b. (Num i, HasZero b) => b -> Matrix i b -> Matrix i b
addColumn b
x Matrix i b
m | b
x forall a. Eq a => a -> a -> Bool
== forall a. HasZero a => a
zeroElement = Matrix i b
m { size :: Size i
size = (forall i b. Matrix i b -> Size i
size Matrix i b
m) { cols :: i
cols = forall i. Size i -> i
cols (forall i b. Matrix i b -> Size i
size Matrix i b
m) forall a. Num a => a -> a -> a
+ i
1 }}
              | Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__

-- | @'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@.

addRow :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b
addRow :: forall i b. (Num i, HasZero b) => b -> Matrix i b -> Matrix i b
addRow b
x Matrix i b
m | b
x forall a. Eq a => a -> a -> Bool
== forall a. HasZero a => a
zeroElement = Matrix i b
m { size :: Size i
size = (forall i b. Matrix i b -> Size i
size Matrix i b
m) { rows :: i
rows = forall i. Size i -> i
rows (forall i b. Matrix i b -> Size i
size Matrix i b
m) forall a. Num a => a -> a -> a
+ i
1 }}
           | Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__

------------------------------------------------------------------------
-- * Printing
------------------------------------------------------------------------

instance (Integral i, HasZero b, Show i, Show b) => Show (Matrix i b) where
  showsPrec :: Int -> Matrix i b -> ShowS
showsPrec Int
_ Matrix i b
m =
    String -> ShowS
showString String
"Agda.Termination.SparseMatrix.fromLists " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows (forall i b. Matrix i b -> Size i
size Matrix i b
m) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows (forall i b. (Integral i, HasZero b) => Matrix i b -> [[b]]
toLists Matrix i b
m)

instance (Integral i, HasZero b, Pretty b) =>
         Pretty (Matrix i b) where
--  pretty = vcat . map (hsep . map pretty) . toLists
  pretty :: Matrix i b -> Doc
pretty = forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. Box -> String
Boxes.render
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *).
Foldable f =>
Int -> Alignment -> f Box -> Box
Boxes.hsep Int
1 Alignment
Boxes.right
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ( forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.right
               forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ( Alignment -> Int -> Box -> Box
Boxes.alignHoriz Alignment
Boxes.right Int
4
                     forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Box
Boxes.text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty
                     )
               )
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i b. (Integral i, HasZero b) => Matrix i b -> [[b]]
toLists
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Transpose a => a -> a
transpose
-- ADAPTED FROM:
-- http://www.tedreed.info/programming/2012/06/02/how-to-use-textprettyprintboxes/
-- print_table :: [[String]] -> IO ()
-- print_table rows = printBox $ hsep 2 left (map (vcat left . map text) (transpose rows))