    {-# 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))