{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Termination.SparseMatrix
(
Matrix(Matrix)
, unM
, Size(..)
, MIx (..)
, fromLists
, fromIndexList
, toLists
, size
, square
, isEmpty
, isSingleton
, zipMatrices
, add
, intersectWith
, interAssocWith
, mul
, transpose
, Diagonal(..)
, toSparseRows
, supSize
, zipAssocWith
, 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
data Size i = Size
{ forall i. Size i -> i
rows :: i
, forall i. Size i -> i
cols :: i
}
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)
data MIx i = MIx
{ forall i. MIx i -> i
row :: i
, forall i. MIx i -> i
col :: i
}
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)
data Matrix i b = Matrix
{ forall i b. Matrix i b -> Size i
size :: Size i
, forall i b. Matrix i b -> [(MIx i, b)]
unM :: [(MIx i, b)]
}
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)
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)
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
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)
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)
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 :: (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)
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
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
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
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
class Diagonal m e | m -> e where
diagonal :: m -> [e]
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
class Transpose a where
transpose :: a -> a
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
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
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
zipAssocWith :: (Ord i)
=> ([(i,a)] -> [(i,c)])
-> ([(i,b)] -> [(i,c)])
-> (a -> Maybe c)
-> (b -> Maybe c)
-> (a -> b -> Maybe c)
-> [(i,a)] -> [(i,b)] -> [(i,c)]
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'
unionAssocWith :: (Ord i)
=> (a -> Maybe c)
-> (b -> Maybe c)
-> (a -> b -> Maybe c)
-> [(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)
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 :: 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 :: (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 :: (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)
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 :: (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
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
onlym :: p -> PartialOrdering
onlym p
o = PartialOrdering
POGT
onlyn :: p -> PartialOrdering
onlyn p
o = PartialOrdering
POLT
both :: a -> a -> PartialOrdering
both = a -> a -> PartialOrdering
forall a. PartialOrd a => Comparable a
comparable
trivial :: PartialOrdering -> Bool
trivial = (PartialOrdering -> PartialOrdering -> Bool
forall a. Eq a => a -> a -> Bool
== PartialOrdering
forall a. Monoid a => a
mempty)
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 :: (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__
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 :: 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