{-# OPTIONS_GHC -Wunused-imports #-}

{- | 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 (on)
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.Syntax.Common.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
(Size i -> Size i -> Bool)
-> (Size i -> Size i -> Bool) -> Eq (Size i)
forall i. Eq i => Size i -> Size i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Size i -> Size i -> Bool
Eq, Eq (Size i)
Eq (Size i) =>
(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)
-> (Size i -> Size i -> Size i)
-> (Size i -> Size i -> Size i)
-> Ord (Size i)
Size i -> Size i -> Bool
Size i -> Size i -> Ordering
Size i -> Size i -> Size i
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
$ccompare :: forall i. Ord i => Size i -> Size i -> Ordering
compare :: Size i -> Size i -> Ordering
$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
>= :: Size i -> Size i -> Bool
$cmax :: forall i. Ord i => Size i -> Size i -> Size i
max :: Size i -> Size i -> Size i
$cmin :: forall i. Ord i => Size i -> Size i -> Size i
min :: Size i -> Size i -> Size i
Ord, Int -> Size i -> ShowS
[Size i] -> ShowS
Size i -> String
(Int -> Size i -> ShowS)
-> (Size i -> String) -> ([Size i] -> ShowS) -> Show (Size i)
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
$cshowsPrec :: forall i. Show i => Int -> Size i -> ShowS
showsPrec :: Int -> Size i -> ShowS
$cshow :: forall i. Show i => Size i -> String
show :: Size i -> String
$cshowList :: forall i. Show i => [Size i] -> ShowS
showList :: [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
(MIx i -> MIx i -> Bool) -> (MIx i -> MIx i -> Bool) -> Eq (MIx i)
forall i. Eq i => MIx i -> MIx i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: MIx i -> MIx i -> Bool
Eq, Eq (MIx i)
Eq (MIx i) =>
(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)
-> (MIx i -> MIx i -> MIx i)
-> (MIx i -> MIx i -> MIx i)
-> Ord (MIx i)
MIx i -> MIx i -> Bool
MIx i -> MIx i -> Ordering
MIx i -> MIx i -> MIx i
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
$ccompare :: forall i. Ord i => MIx i -> MIx i -> Ordering
compare :: MIx i -> MIx i -> Ordering
$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
>= :: MIx i -> MIx i -> Bool
$cmax :: forall i. Ord i => MIx i -> MIx i -> MIx i
max :: MIx i -> MIx i -> MIx i
$cmin :: forall i. Ord i => MIx i -> MIx i -> MIx i
min :: MIx i -> MIx i -> MIx i
Ord, Int -> MIx i -> ShowS
[MIx i] -> ShowS
MIx i -> String
(Int -> MIx i -> ShowS)
-> (MIx i -> String) -> ([MIx i] -> ShowS) -> Show (MIx i)
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
$cshowsPrec :: forall i. Show i => Int -> MIx i -> ShowS
showsPrec :: Int -> MIx i -> ShowS
$cshow :: forall i. Show i => MIx i -> String
show :: MIx i -> String
$cshowList :: forall i. Show i => [MIx i] -> ShowS
showList :: [MIx i] -> ShowS
Show, Ord (MIx i)
Ord (MIx i) =>
((MIx i, MIx i) -> [MIx i])
-> ((MIx i, MIx i) -> MIx i -> Int)
-> ((MIx i, MIx i) -> MIx i -> Int)
-> ((MIx i, MIx i) -> MIx i -> Bool)
-> ((MIx i, MIx i) -> Int)
-> ((MIx i, MIx i) -> Int)
-> Ix (MIx i)
(MIx i, MIx i) -> Int
(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
$crange :: forall i. Ix i => (MIx i, MIx i) -> [MIx i]
range :: (MIx i, MIx i) -> [MIx i]
$cindex :: forall i. Ix i => (MIx i, MIx i) -> MIx i -> Int
index :: (MIx i, MIx i) -> MIx i -> Int
$cunsafeIndex :: forall i. Ix i => (MIx i, MIx i) -> MIx i -> Int
unsafeIndex :: (MIx i, MIx i) -> MIx i -> Int
$cinRange :: forall i. Ix i => (MIx i, MIx i) -> MIx i -> Bool
inRange :: (MIx i, MIx i) -> MIx i -> Bool
$crangeSize :: forall i. Ix i => (MIx i, MIx i) -> Int
rangeSize :: (MIx i, MIx i) -> Int
$cunsafeRangeSize :: forall i. Ix i => (MIx i, MIx i) -> Int
unsafeRangeSize :: (MIx i, MIx i) -> Int
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
(Matrix i b -> Matrix i b -> Bool)
-> (Matrix i b -> Matrix i b -> Bool) -> Eq (Matrix i b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i b. (Eq i, Eq b) => 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
/= :: Matrix i b -> Matrix i b -> Bool
Eq, Eq (Matrix i b)
Eq (Matrix i b) =>
(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)
-> (Matrix i b -> Matrix i b -> Matrix i b)
-> (Matrix i b -> Matrix i b -> Matrix i b)
-> Ord (Matrix i b)
Matrix i b -> Matrix i b -> Bool
Matrix i b -> Matrix i b -> Ordering
Matrix i b -> Matrix i b -> Matrix i b
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
$ccompare :: forall i b. (Ord i, Ord b) => Matrix i b -> Matrix i b -> Ordering
compare :: Matrix i b -> Matrix i b -> Ordering
$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
>= :: Matrix i b -> Matrix i b -> Bool
$cmax :: 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
$cmin :: 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
Ord, (forall a b. (a -> b) -> Matrix i a -> Matrix i b)
-> (forall a b. a -> Matrix i b -> Matrix i a)
-> Functor (Matrix i)
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
$cfmap :: forall i a b. (a -> b) -> Matrix i a -> Matrix i b
fmap :: forall a b. (a -> b) -> Matrix i a -> Matrix i b
$c<$ :: forall i a b. a -> Matrix i b -> Matrix i a
<$ :: forall a b. a -> Matrix i b -> Matrix i a
Functor, (forall m. Monoid m => Matrix i m -> m)
-> (forall m a. Monoid m => (a -> m) -> Matrix i a -> m)
-> (forall m a. Monoid m => (a -> m) -> Matrix i a -> m)
-> (forall a b. (a -> b -> b) -> b -> Matrix i a -> b)
-> (forall a b. (a -> b -> b) -> b -> Matrix i a -> b)
-> (forall b a. (b -> a -> b) -> b -> Matrix i a -> b)
-> (forall b a. (b -> a -> b) -> b -> Matrix i a -> b)
-> (forall a. (a -> a -> a) -> Matrix i a -> a)
-> (forall a. (a -> a -> a) -> Matrix i a -> a)
-> (forall a. Matrix i a -> [a])
-> (forall a. Matrix i a -> Bool)
-> (forall a. Matrix i a -> Int)
-> (forall a. Eq a => a -> Matrix i a -> Bool)
-> (forall a. Ord a => Matrix i a -> a)
-> (forall a. Ord a => Matrix i a -> a)
-> (forall a. Num a => Matrix i a -> a)
-> (forall a. Num a => Matrix i a -> a)
-> Foldable (Matrix i)
forall a. Eq a => a -> Matrix i a -> Bool
forall a. Num a => Matrix i a -> a
forall a. Ord a => Matrix i a -> a
forall m. Monoid m => Matrix i m -> m
forall a. Matrix i a -> Bool
forall a. Matrix i a -> Int
forall a. Matrix i a -> [a]
forall a. (a -> a -> a) -> Matrix i a -> a
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 b a. (b -> a -> b) -> b -> Matrix i a -> b
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
$cfold :: forall i m. Monoid m => Matrix i m -> m
fold :: forall m. Monoid m => Matrix i m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Matrix i a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Matrix i a -> b
$cfoldr1 :: forall i a. (a -> a -> a) -> Matrix i a -> a
foldr1 :: forall a. (a -> a -> a) -> Matrix i a -> a
$cfoldl1 :: forall i a. (a -> a -> a) -> Matrix i a -> a
foldl1 :: forall a. (a -> a -> a) -> Matrix i a -> a
$ctoList :: forall i a. Matrix i a -> [a]
toList :: forall a. Matrix i a -> [a]
$cnull :: forall i a. Matrix i a -> Bool
null :: forall a. Matrix i a -> Bool
$clength :: forall i a. Matrix i a -> Int
length :: forall a. Matrix i a -> Int
$celem :: forall i a. Eq a => a -> Matrix i a -> Bool
elem :: forall a. Eq a => a -> Matrix i a -> Bool
$cmaximum :: forall i a. Ord a => Matrix i a -> a
maximum :: forall a. Ord a => Matrix i a -> a
$cminimum :: forall i a. Ord a => Matrix i a -> a
minimum :: forall a. Ord a => Matrix i a -> a
$csum :: forall i a. Num a => Matrix i a -> a
sum :: forall a. Num a => Matrix i a -> a
$cproduct :: forall i a. Num a => Matrix i a -> a
product :: forall a. Num a => Matrix i a -> a
Foldable, Functor (Matrix i)
Foldable (Matrix i)
(Functor (Matrix i), Foldable (Matrix i)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Matrix i a -> f (Matrix i b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Matrix i (f a) -> f (Matrix i a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Matrix i a -> m (Matrix i b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Matrix i (m a) -> m (Matrix i a))
-> Traversable (Matrix i)
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 (m :: * -> *) a. Monad m => Matrix i (m a) -> m (Matrix i a)
forall (f :: * -> *) a.
Applicative f =>
Matrix i (f a) -> f (Matrix i a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Matrix i a -> m (Matrix i b)
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)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Matrix i a -> f (Matrix i b)
$csequenceA :: forall i (f :: * -> *) a.
Applicative f =>
Matrix i (f a) -> f (Matrix i a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Matrix i (f a) -> f (Matrix i a)
$cmapM :: forall i (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Matrix i a -> m (Matrix i b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Matrix i a -> m (Matrix i b)
$csequence :: forall i (m :: * -> *) a.
Monad m =>
Matrix i (m a) -> m (Matrix i a)
sequence :: forall (m :: * -> *) a. Monad m => Matrix i (m a) -> m (Matrix i a)
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 = Size i -> i
forall i. Size i -> i
rows (Matrix i b -> Size i
forall i b. Matrix i b -> Size i
size Matrix i b
m) i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== Size i -> i
forall i. Size i -> i
cols (Matrix i b -> Size i
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 = Size i -> i
forall i. Size i -> i
rows Size i
sz i -> i -> Bool
forall a. Ord a => a -> a -> Bool
<= i
0 Bool -> Bool -> Bool
|| Size i -> i
forall i. Size i -> i
cols Size i
sz i -> i -> Bool
forall a. Ord a => a -> a -> Bool
<= i
0
  where sz :: Size i
sz = Matrix i b -> Size i
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)]
_) =
  i -> i -> Size i
forall i. i -> i -> Size i
Size (i -> i -> i
forall a. Ord a => a -> a -> a
max i
r1 i
r2) (i -> i -> i
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)]
_) =
  i -> i -> Size i
forall i. i -> i -> Size i
Size (i -> i -> i
forall a. Ord a => a -> a -> a
min i
r1 i
r2) (i -> i -> i
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 = Size i -> [(MIx i, b)] -> Matrix i b
forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix Size i
sz
                 ([(MIx i, b)] -> Matrix i b)
-> ([(MIx i, b)] -> [(MIx i, b)]) -> [(MIx i, b)] -> Matrix i b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((MIx i, b) -> (MIx i, b) -> Ordering)
-> [(MIx i, b)] -> [(MIx i, b)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (MIx i -> MIx i -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (MIx i -> MIx i -> Ordering)
-> ((MIx i, b) -> MIx i) -> (MIx i, b) -> (MIx i, b) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (MIx i, b) -> MIx i
forall a b. (a, b) -> a
fst)
                 ([(MIx i, b)] -> [(MIx i, b)])
-> ([(MIx i, b)] -> [(MIx i, b)]) -> [(MIx i, b)] -> [(MIx i, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((MIx i, b) -> Bool) -> [(MIx i, b)] -> [(MIx i, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((b
forall a. HasZero a => a
zeroElement b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/=) (b -> Bool) -> ((MIx i, b) -> b) -> (MIx i, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MIx i, b) -> b
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 = Size i -> [(MIx i, b)] -> Matrix i b
forall i b.
(Ord i, HasZero b) =>
Size i -> [(MIx i, b)] -> Matrix i b
fromIndexList Size i
sz ([(MIx i, b)] -> Matrix i b) -> [(MIx i, b)] -> Matrix i b
forall a b. (a -> b) -> a -> b
$ [MIx i] -> [b] -> [(MIx i, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([ i -> i -> MIx i
forall i. i -> i -> MIx i
MIx i
i i
j | i
i <- [i
1..Size i -> i
forall i. Size i -> i
rows Size i
sz]
                                                    , i
j <- [i
1..Size i -> i
forall i. Size i -> i
cols Size i
sz]]) ([[b]] -> [b]
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)) = i -> [(i, b)] -> [(MIx i, b)] -> [(i, [(i, b)])]
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', [(a, b)] -> [(a, b)]
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' a -> a -> Bool
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)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
row) [(MIx a, b)]
m
          | Bool
otherwise = (a
i', [(a, b)] -> [(a, b)]
forall a. [a] -> [a]
reverse [(a, b)]
row) (a, [(a, b)]) -> [(a, [(a, b)])] -> [(a, [(a, b)])]
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 []           = i -> b -> [b]
forall i a. Integral i => i -> a -> [a]
List.genericReplicate (i
n i -> i -> i
forall a. Num a => a -> a -> a
+ i
1 i -> i -> i
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 i -> i -> Bool
forall a. Ord a => a -> a -> Bool
> i
j Bool -> Bool -> Bool
|| i
i i -> i -> Bool
forall a. Ord a => a -> a -> Bool
> i
n = [b]
forall a. HasCallStack => a
__IMPOSSIBLE__
          | i
i i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== i
j         = b
b    b -> [b] -> [b]
forall a. a -> [a] -> [a]
: i -> [(i, b)] -> [b]
aux (i
i i -> i -> i
forall a. Num a => a -> a -> a
+ i
1) [(i, b)]
l'
          | Bool
otherwise      = b
zero b -> [b] -> [b]
forall a. a -> [a] -> [a]
: i -> [(i, b)] -> [b]
aux (i
i i -> 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)]
_) =
    [b] -> i -> [(i, [b])] -> [[b]]
forall i b. Integral i => b -> i -> [(i, b)] -> [b]
blowUpSparseVec [b]
emptyRow i
nrows ([(i, [b])] -> [[b]]) -> [(i, [b])] -> [[b]]
forall a b. (a -> b) -> a -> b
$
      ((i, [(i, b)]) -> (i, [b])) -> [(i, [(i, b)])] -> [(i, [b])]
forall a b. (a -> b) -> [a] -> [b]
map (([(i, b)] -> [b]) -> (i, [(i, b)]) -> (i, [b])
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (b -> i -> [(i, b)] -> [b]
forall i b. Integral i => b -> i -> [(i, b)] -> [b]
blowUpSparseVec b
forall a. HasZero a => a
zeroElement i
ncols)) ([(i, [(i, b)])] -> [(i, [b])]) -> [(i, [(i, b)])] -> [(i, [b])]
forall a b. (a -> b) -> a -> b
$ Matrix i b -> [(i, [(i, b)])]
forall i b. Eq i => Matrix i b -> [(i, [(i, b)])]
toSparseRows Matrix i b
m
  where
    emptyRow :: [b]
emptyRow = i -> b -> [b]
forall i a. Integral i => i -> a -> [a]
List.genericReplicate i
ncols b
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)]) = b -> Maybe b
forall a. a -> Maybe a
Just b
b
isSingleton (Matrix (Size i
1 i
1) []     ) = b -> Maybe b
forall a. a -> Maybe a
Just b
forall a. HasZero a => a
zeroElement
isSingleton (Matrix (Size i
1 i
1) [(MIx i, b)]
_      ) = Maybe b
forall a. HasCallStack => a
__IMPOSSIBLE__
isSingleton Matrix i b
_ = Maybe 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) =
    b -> i -> [(i, b)] -> [b]
forall i b. Integral i => b -> i -> [(i, b)] -> [b]
blowUpSparseVec b
forall a. HasZero a => a
zeroElement (i -> i -> i
forall a. Ord a => a -> a -> a
min i
r i
c) ([(i, b)] -> [b]) -> [(i, b)] -> [b]
forall a b. (a -> b) -> a -> b
$
      ((MIx i, b) -> Maybe (i, b)) -> [(MIx i, b)] -> [(i, b)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (MIx i
i i
j, b
b) -> if i
i i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== i
j then (i, b) -> Maybe (i, b)
forall a. a -> Maybe a
Just (i
i, b
b) else Maybe (i, b)
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) = i -> i -> Size i
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) = i -> i -> MIx i
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) =
    Size i -> [(MIx i, b)] -> Matrix i b
forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix (Size i -> Size i
forall a. Transpose a => a -> a
transpose Size i
size) ([(MIx i, b)] -> Matrix i b) -> [(MIx i, b)] -> Matrix i b
forall a b. (a -> b) -> a -> b
$
      ((MIx i, b) -> (MIx i, b) -> Ordering)
-> [(MIx i, b)] -> [(MIx i, b)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (MIx i -> MIx i -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (MIx i -> MIx i -> Ordering)
-> ((MIx i, b) -> MIx i) -> (MIx i, b) -> (MIx i, b) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (MIx i, b) -> MIx i
forall a b. (a, b) -> a
fst) ([(MIx i, b)] -> [(MIx i, b)]) -> [(MIx i, b)] -> [(MIx i, b)]
forall a b. (a -> b) -> a -> b
$
        ((MIx i, b) -> (MIx i, b)) -> [(MIx i, b)] -> [(MIx i, b)]
forall a b. (a -> b) -> [a] -> [b]
map ((MIx i -> MIx i) -> (MIx i, b) -> (MIx i, b)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst MIx i -> MIx i
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 [] = ((i, a) -> Maybe (i, c)) -> [(i, a)] -> [(i, c)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (i
i, a
a) -> (i
i,) (c -> (i, c)) -> Maybe c -> Maybe (i, c)
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 = ((i, b) -> Maybe (i, c)) -> [(i, b)] -> [(i, c)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (i
i, b
b) -> (i
i,) (c -> (i, c)) -> Maybe c -> Maybe (i, c)
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 i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
compare i
i i
j of
        Ordering
LT -> Maybe (i, c) -> [(i, c)] -> [(i, c)]
forall a. Maybe a -> [a] -> [a]
mcons ((i
i,) (c -> (i, c)) -> Maybe c -> Maybe (i, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe c
f a
a)   ([(i, c)] -> [(i, c)]) -> [(i, c)] -> [(i, c)]
forall a b. (a -> b) -> a -> b
$ [(i, a)] -> [(i, b)] -> [(i, c)]
merge [(i, a)]
m1' [(i, b)]
m2
        Ordering
GT -> Maybe (i, c) -> [(i, c)] -> [(i, c)]
forall a. Maybe a -> [a] -> [a]
mcons ((i
j,) (c -> (i, c)) -> Maybe c -> Maybe (i, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> Maybe c
g b
b)   ([(i, c)] -> [(i, c)]) -> [(i, c)] -> [(i, c)]
forall a b. (a -> b) -> a -> b
$ [(i, a)] -> [(i, b)] -> [(i, c)]
merge [(i, a)]
m1  [(i, b)]
m2'
        Ordering
EQ -> Maybe (i, c) -> [(i, c)] -> [(i, c)]
forall a. Maybe a -> [a] -> [a]
mcons ((i
i,) (c -> (i, c)) -> Maybe c -> Maybe (i, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> Maybe c
h a
a b
b) ([(i, c)] -> [(i, c)]) -> [(i, c)] -> [(i, c)]
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 = ([(i, a)] -> [(i, c)])
-> ([(i, b)] -> [(i, c)])
-> (a -> Maybe c)
-> (b -> Maybe c)
-> (a -> b -> Maybe c)
-> [(i, a)]
-> [(i, b)]
-> [(i, c)]
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 ((a -> Maybe c) -> [(i, a)] -> [(i, c)]
forall {t} {a} {t}. (t -> Maybe a) -> [(t, t)] -> [(t, a)]
map_ a -> Maybe c
f) ((b -> Maybe c) -> [(i, b)] -> [(i, c)]
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 = ((t, t) -> Maybe (t, a)) -> [(t, t)] -> [(t, a)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (t
i, t
a) -> (t
i,) (a -> (t, a)) -> Maybe a -> Maybe (t, a)
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 = Size i -> [(MIx i, c)] -> Matrix i c
forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix (Matrix i a -> Matrix i b -> Size i
forall i a b. Ord i => Matrix i a -> Matrix i b -> Size i
supSize Matrix i a
m1 Matrix i b
m2) ([(MIx i, c)] -> Matrix i c) -> [(MIx i, c)] -> Matrix i c
forall a b. (a -> b) -> a -> b
$
  (a -> Maybe c)
-> (b -> Maybe c)
-> (a -> b -> Maybe c)
-> [(MIx i, a)]
-> [(MIx i, b)]
-> [(MIx i, c)]
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 (c -> Maybe c) -> (a -> c) -> a -> Maybe c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> c
f) (c -> Maybe c
drop0 (c -> Maybe c) -> (b -> c) -> b -> Maybe c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c
g) (\ a
a -> c -> Maybe c
drop0 (c -> Maybe c) -> (b -> c) -> b -> Maybe c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c
h a
a) (Matrix i a -> [(MIx i, a)]
forall i b. Matrix i b -> [(MIx i, b)]
unM Matrix i a
m1) (Matrix i b -> [(MIx i, b)]
forall i b. Matrix i b -> [(MIx i, b)]
unM Matrix i b
m2)
  where
    drop0 :: c -> Maybe c
drop0 = (c -> Bool) -> c -> Maybe c
forall a. (a -> Bool) -> a -> Maybe a
filterMaybe (Bool -> Bool
not (Bool -> Bool) -> (c -> Bool) -> c -> Bool
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 = (a -> a)
-> (a -> a)
-> (a -> a -> a)
-> (a -> Bool)
-> Matrix i a
-> Matrix i a
-> Matrix i a
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 -> a
forall a. a -> a
id a -> a
forall a. a -> a
id a -> a -> a
plus (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
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 = Size i -> [(MIx i, a)] -> Matrix i a
forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix (Matrix i a -> Matrix i a -> Size i
forall i a b. Ord i => Matrix i a -> Matrix i b -> Size i
infSize Matrix i a
m1 Matrix i a
m2) ([(MIx i, a)] -> Matrix i a) -> [(MIx i, a)] -> Matrix i a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> [(MIx i, a)] -> [(MIx i, a)] -> [(MIx i, a)]
forall i a.
Ord i =>
(a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
interAssocWith a -> a -> a
f (Matrix i a -> [(MIx i, a)]
forall i b. Matrix i b -> [(MIx i, b)]
unM Matrix i a
m1) (Matrix i a -> [(MIx i, a)]
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 i -> i -> Bool
forall a. Ord a => a -> a -> Bool
< i
j = (a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, 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
    | i
i i -> i -> Bool
forall a. Ord a => a -> a -> Bool
> i
j = (a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, 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'
    | Bool
otherwise = (i
i, a -> a -> a
f a
a a
b) (i, a) -> [(i, a)] -> [(i, a)]
forall a. a -> [a] -> [a]
: (a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, 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 = Size i -> [(MIx i, a)] -> Matrix i a
forall i b. Size i -> [(MIx i, b)] -> Matrix i b
Matrix (Size { rows :: i
rows = Size i -> i
forall i. Size i -> i
rows (Matrix i a -> Size i
forall i b. Matrix i b -> Size i
size Matrix i a
m1), cols :: i
cols = Size i -> i
forall i. Size i -> i
cols (Matrix i a -> Size i
forall i b. Matrix i b -> Size i
size Matrix i a
m2) }) ([(MIx i, a)] -> Matrix i a) -> [(MIx i, a)] -> Matrix i a
forall a b. (a -> b) -> a -> b
$
  [ (i -> i -> MIx i
forall i. i -> i -> MIx i
MIx i
i i
j, a
b)
    | (i
i,[(i, a)]
v) <- Matrix i a -> [(i, [(i, a)])]
forall i b. Eq i => Matrix i b -> [(i, [(i, b)])]
toSparseRows Matrix i a
m1
    , (i
j,[(i, a)]
w) <- Matrix i a -> [(i, [(i, a)])]
forall i b. Eq i => Matrix i b -> [(i, [(i, b)])]
toSparseRows (Matrix i a -> [(i, [(i, a)])]) -> Matrix i a -> [(i, [(i, a)])]
forall a b. (a -> b) -> a -> b
$ Matrix i a -> Matrix i a
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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
zero
  ]
  where
     zero :: a
zero  = Semiring a -> a
forall a. Semiring a -> a
Semiring.zero Semiring a
semiring
     plus :: a -> a -> a
plus  = Semiring a -> a -> a -> a
forall a. Semiring a -> a -> a -> a
Semiring.add  Semiring a
semiring
     times :: a -> a -> a
times = Semiring a -> a -> a -> a
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 = (a -> a -> a) -> a -> [a] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' a -> a -> a
plus a
zero ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$
                   ((i, a) -> a) -> [(i, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (i, a) -> a
forall a b. (a, b) -> b
snd ([(i, a)] -> [a]) -> [(i, a)] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
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
    | Matrix i a -> Size i
forall i b. Matrix i b -> Size i
size Matrix i a
m Size i -> Size i -> Bool
forall a. Eq a => a -> a -> Bool
/= Matrix i a -> Size i
forall i b. Matrix i b -> Size i
size Matrix i a
n = PartialOrdering
POAny
    | Bool
otherwise        = Matrix i PartialOrdering -> PartialOrdering
forall m. Monoid m => Matrix i m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold (Matrix i PartialOrdering -> PartialOrdering)
-> Matrix i PartialOrdering -> PartialOrdering
forall a b. (a -> b) -> a -> b
$
                           (a -> PartialOrdering)
-> (a -> PartialOrdering)
-> (a -> a -> PartialOrdering)
-> (PartialOrdering -> Bool)
-> Matrix i a
-> Matrix i a
-> Matrix i PartialOrdering
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 -> PartialOrdering
forall {p}. p -> PartialOrdering
onlym a -> PartialOrdering
forall {p}. p -> PartialOrdering
onlyn a -> a -> PartialOrdering
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 :: a -> a -> PartialOrdering
both    = a -> a -> PartialOrdering
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 = (PartialOrdering -> PartialOrdering -> Bool
forall a. Eq a => a -> a -> Bool
== PartialOrdering
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 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall a. HasZero a => a
zeroElement = Matrix i b
m { size = (size m) { cols = cols (size m) + 1 }}
              | Bool
otherwise = Matrix i b
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 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall a. HasZero a => a
zeroElement = Matrix i b
m { size = (size m) { rows = rows (size m) + 1 }}
           | Bool
otherwise = Matrix i b
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 " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size i -> ShowS
forall a. Show a => a -> ShowS
shows (Matrix i b -> Size i
forall i b. Matrix i b -> Size i
size Matrix i b
m) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[b]] -> ShowS
forall a. Show a => a -> ShowS
shows (Matrix i b -> [[b]]
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 = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
         ([Doc] -> Doc) -> (Matrix i b -> [Doc]) -> Matrix i b -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
forall a. String -> Doc a
text
         ([String] -> [Doc])
-> (Matrix i b -> [String]) -> Matrix i b -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines
         (String -> [String])
-> (Matrix i b -> String) -> Matrix i b -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Box -> String
Boxes.render
         (Box -> String) -> (Matrix i b -> Box) -> Matrix i b -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Alignment -> [Box] -> Box
forall (f :: * -> *).
Foldable f =>
Int -> Alignment -> f Box -> Box
Boxes.hsep Int
1 Alignment
Boxes.right
         ([Box] -> Box) -> (Matrix i b -> [Box]) -> Matrix i b -> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([b] -> Box) -> [[b]] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map ( Alignment -> [Box] -> Box
forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.right
               ([Box] -> Box) -> ([b] -> [Box]) -> [b] -> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Box) -> [b] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map ( Alignment -> Int -> Box -> Box
Boxes.alignHoriz Alignment
Boxes.right Int
4
                     (Box -> Box) -> (b -> Box) -> b -> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Box
Boxes.text (String -> Box) -> (b -> String) -> b -> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Doc a -> String
render (Doc -> String) -> (b -> Doc) -> b -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Doc
forall a. Pretty a => a -> Doc
pretty
                     )
               )
         ([[b]] -> [Box]) -> (Matrix i b -> [[b]]) -> Matrix i b -> [Box]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Matrix i b -> [[b]]
forall i b. (Integral i, HasZero b) => Matrix i b -> [[b]]
toLists
         (Matrix i b -> [[b]])
-> (Matrix i b -> Matrix i b) -> Matrix i b -> [[b]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Matrix i b -> Matrix i b
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))