{-# LANGUAGE CPP #-}
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
import qualified Data.List as List
import Data.Maybe
import Data.Monoid
import Data.Foldable (Foldable)
import qualified Data.Foldable as Fold
import Data.Traversable (Traversable)
import qualified Text.PrettyPrint.Boxes as Boxes
import Agda.Termination.Semiring (HasZero(..), Semiring)
import qualified Agda.Termination.Semiring as Semiring
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.PartialOrd
import Agda.Utils.Pretty hiding (isEmpty)
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
data Size i = Size
{ rows :: i
, cols :: i
}
deriving (Eq, Ord, Show)
data MIx i = MIx
{ row :: i
, col :: i
}
deriving (Eq, Ord, Show, Ix)
toBounds :: Num i => Size i -> (MIx i, MIx i)
toBounds sz = (MIx { row = 1, col = 1 }, MIx { row = rows sz, col = cols sz })
data Matrix i b = Matrix
{ size :: Size i
, unM :: [(MIx i, b)]
}
deriving (Eq, Ord, Functor, Foldable, Traversable)
square :: Ix i => Matrix i b -> Bool
square m = rows (size m) == cols (size m)
isEmpty :: (Num i, Ix i) => Matrix i b -> Bool
isEmpty m = rows sz <= 0 || cols sz <= 0
where sz = size m
supSize :: Ord i => Matrix i a -> Matrix i b -> Size i
supSize (Matrix (Size r1 c1) _) (Matrix (Size r2 c2) _) =
Size (max r1 r2) (max c1 c2)
infSize :: Ord i => Matrix i a -> Matrix i b -> Size i
infSize (Matrix (Size r1 c1) _) (Matrix (Size r2 c2) _) =
Size (min r1 r2) (min c1 c2)
fromIndexList :: (Ord i, HasZero b) => Size i -> [(MIx i, b)] -> Matrix i b
fromIndexList sz = Matrix sz
. List.sortBy (compare `on` fst)
. filter ((zeroElement /=) . snd)
fromLists :: (Ord i, Num i, Enum i, HasZero b) => Size i -> [[b]] -> Matrix i b
fromLists sz bs = fromIndexList sz $ zip ([ MIx i j | i <- [1..rows sz]
, j <- [1..cols sz]]) (concat bs)
toSparseRows :: (Eq i) => Matrix i b -> [(i,[(i,b)])]
toSparseRows (Matrix _ []) = []
toSparseRows (Matrix _ ((MIx i j, b) : m)) = aux i [(j,b)] m
where aux i' [] [] = []
aux i' row [] = [(i', reverse row)]
aux i' row ((MIx i j, b) : m)
| i' == i = aux i' ((j,b):row) m
| otherwise = (i', reverse row) : aux i [(j,b)] m
blowUpSparseVec :: (Integral i) => b -> i -> [(i,b)] -> [b]
blowUpSparseVec zero n l = aux 1 l
where aux i [] = List.genericReplicate (n + 1 - i) zero
aux i l@((j,b):l')
| i > j || i > n = __IMPOSSIBLE__
| i == j = b : aux (i + 1) l'
| otherwise = zero : aux (i + 1) l
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__
toLists :: (Integral i, HasZero b) => Matrix i b -> [[b]]
toLists m@(Matrix size@(Size nrows ncols) _) =
blowUpSparseVec emptyRow nrows $
map (mapSnd (blowUpSparseVec zeroElement ncols)) $ toSparseRows m
where
emptyRow = List.genericReplicate ncols zeroElement
isSingleton :: (Eq i, Num i, HasZero b) => Matrix i b -> Maybe b
isSingleton (Matrix (Size 1 1) [(_,b)]) = Just b
isSingleton (Matrix (Size 1 1) [] ) = Just zeroElement
isSingleton (Matrix (Size 1 1) _ ) = __IMPOSSIBLE__
isSingleton _ = Nothing
class Diagonal m e | m -> e where
diagonal :: m -> [e]
instance (Integral i, HasZero b) => Diagonal (Matrix i b) b where
diagonal (Matrix (Size r c) m) =
blowUpSparseVec zeroElement (min r c) $
mapMaybe (\ ((MIx i j), b) -> if i==j then Just (i,b) else Nothing) m
class Transpose a where
transpose :: a -> a
instance Transpose (Size i) where
transpose (Size n m) = Size m n
instance Transpose (MIx i) where
transpose (MIx i j) = MIx j i
instance Ord i => Transpose (Matrix i b) where
transpose (Matrix size m) =
Matrix (transpose size) $
List.sortBy (compare `on` fst) $
map (mapFst transpose) 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 fs gs f g h = merge
where
merge m1 [] = mapMaybe (\ (i, a) -> (i,) <$> f a) m1
merge [] m2 = mapMaybe (\ (i, b) -> (i,) <$> g b) m2
merge m1@((i,a):m1') m2@((j,b):m2') =
case compare i j of
LT -> mcons ((i,) <$> f a) $ merge m1' m2
GT -> mcons ((j,) <$> g b) $ merge m1 m2'
EQ -> mcons ((i,) <$> h a b) $ merge m1' m2'
unionAssocWith :: (Ord i)
=> (a -> Maybe c)
-> (b -> Maybe c)
-> (a -> b -> Maybe c)
-> [(i,a)] -> [(i,b)] -> [(i,c)]
unionAssocWith f g h = zipAssocWith (map_ f) (map_ g) f g h
where
map_ f = mapMaybe (\ (i, a) -> (i,) <$> f 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 f g h zero m1 m2 = Matrix (supSize m1 m2) $
unionAssocWith (drop0 . f) (drop0 . g) (\ a -> drop0 . h a) (unM m1) (unM m2)
where
drop0 = filterMaybe (not . zero)
add :: (Ord i, HasZero a) => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
add plus = zipMatrices id id plus (== zeroElement)
intersectWith :: (Ord i) => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
intersectWith f m1 m2 = Matrix (infSize m1 m2) $ interAssocWith f (unM m1) (unM m2)
interAssocWith :: (Ord i) => (a -> a -> a) -> [(i,a)] -> [(i,a)] -> [(i,a)]
interAssocWith f [] m = []
interAssocWith f l [] = []
interAssocWith f l@((i,a):l') m@((j,b):m')
| i < j = interAssocWith f l' m
| i > j = interAssocWith f l m'
| otherwise = (i, f a b) : interAssocWith f l' m'
mul :: (Ix i, Eq a)
=> Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
mul semiring m1 m2 = Matrix (Size { rows = rows (size m1), cols = cols (size m2) }) $
[ (MIx i j, b)
| (i,v) <- toSparseRows m1
, (j,w) <- toSparseRows $ transpose m2
, let b = inner v w
, b /= zero
]
where
zero = Semiring.zero semiring
plus = Semiring.add semiring
times = Semiring.mul semiring
inner v w = List.foldl' plus zero $
map snd $ interAssocWith times v w
instance (Ord i, PartialOrd a) => PartialOrd (Matrix i a) where
comparable m n
| size m /= size n = POAny
| otherwise = Fold.fold $
zipMatrices onlym onlyn both trivial m n
where
onlym o = POGT
onlyn o = POLT
both = comparable
trivial = (==mempty)
addColumn :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b
addColumn x m | x == zeroElement = m { size = (size m) { cols = cols (size m) + 1 }}
| otherwise = __IMPOSSIBLE__
addRow :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b
addRow x m | x == zeroElement = m { size = (size m) { rows = rows (size m) + 1 }}
| otherwise = __IMPOSSIBLE__
instance (Integral i, HasZero b, Show i, Show b) => Show (Matrix i b) where
showsPrec _ m =
showString "Agda.Termination.SparseMatrix.fromLists " . shows (size m) .
showString " " . shows (toLists m)
instance (Integral i, HasZero b, Pretty b) =>
Pretty (Matrix i b) where
pretty = vcat
. map text
. lines
. Boxes.render
. Boxes.hsep 1 Boxes.right
. map ( Boxes.vcat Boxes.right
. map ( Boxes.alignHoriz Boxes.right 4
. Boxes.text . render . pretty
)
)
. toLists
. transpose