module Agda.Utils.Graph.AdjacencyMap.Unidirectional
( Graph(..)
, Edge(..)
, transposeEdge
, edges
, edgesFrom
, edgesTo
, diagonal
, lookup
, neighbours, neighboursMap
, sourceNodes, targetNodes
, Nodes(..)
, computeNodes, nodes
, fromNodes
, fromList, fromListWith
, toList
, discrete
, clean
, empty
, singleton
, insert, insertWith
, insertEdge, insertEdgeWith
, union , unionWith
, unions, unionsWith
, removeNode
, removeEdge
, filterEdges
, unzip
, mapWithEdge
, sccs'
, sccs
, DAG(..)
, dagInvariant
, oppositeDAG
, reachable
, sccDAG'
, sccDAG
, acyclic
, reachableFrom
, walkSatisfying
, composeWith
, complete
, gaussJordanFloydWarshallMcNaughtonYamadaReference
, gaussJordanFloydWarshallMcNaughtonYamada
)
where
import Prelude hiding (lookup, unzip, null)
import Control.Applicative hiding (empty)
import Control.Monad
import qualified Data.Array.IArray as Array
import qualified Data.Edison.Seq.BankersQueue as BQ
import qualified Data.Edison.Seq.SimpleQueue as SQ
import Data.Function
import qualified Data.Graph as Graph
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import qualified Data.Map.Strict as Map
import Data.Map.Strict (Map)
import qualified Data.Maybe as Maybe
import Data.Maybe (maybeToList, fromMaybe, catMaybes)
import qualified Data.Set as Set
import Data.Set (Set)
import qualified Data.Tree as Tree
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List (headMaybe)
import Agda.Utils.Null (Null(null))
import qualified Agda.Utils.Null as Null
import Agda.Utils.SemiRing
import Agda.Utils.Singleton (Singleton)
import qualified Agda.Utils.Singleton as Singleton
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
newtype Graph s t e = Graph
{ graph :: Map s (Map t e)
}
deriving (Eq, Functor, Show)
data Edge s t e = Edge
{ source :: s
, target :: t
, label :: e
} deriving (Eq, Ord, Functor, Show)
transposeEdge :: Edge s t e -> Edge t s e
transposeEdge (Edge s t e) = Edge t s e
edges :: Graph s t e -> [Edge s t e]
edges (Graph g) =
[ Edge s t e
| (s, tes) <- Map.assocs g
, (t, e) <- Map.assocs tes
]
edgesFrom :: Ord s => Graph s t e -> [s] -> [Edge s t e]
edgesFrom (Graph g) ss =
[ Edge s t e
| s <- ss
, m <- maybeToList $ Map.lookup s g
, (t, e) <- Map.assocs m
]
edgesTo :: Ord t => Graph s t e -> [t] -> [Edge s t e]
edgesTo (Graph g) ts =
[ Edge s t e
| (s, m) <- Map.assocs g
, t <- ts
, e <- maybeToList $ Map.lookup t m
]
diagonal :: (Ord n) => Graph n n e -> [Edge n n e]
diagonal (Graph g) =
[ Edge s s e
| (s, m) <- Map.assocs g
, e <- maybeToList $ Map.lookup s m
]
lookup :: (Ord s, Ord t) => s -> t -> Graph s t e -> Maybe e
lookup s t (Graph g) = Map.lookup t =<< Map.lookup s g
neighbours :: Ord s => s -> Graph s t e -> [(t, e)]
neighbours s (Graph g) = maybe [] Map.assocs $ Map.lookup s g
neighboursMap :: Ord s => s -> Graph s t e -> Map t e
neighboursMap s (Graph g) = fromMaybe Map.empty $ Map.lookup s g
sourceNodes :: Graph s t e -> Set s
sourceNodes = Map.keysSet . graph
targetNodes :: Ord t => Graph s t e -> Set t
targetNodes = Set.fromList . map target . edges
data Nodes n = Nodes
{ srcNodes :: Set n
, tgtNodes :: Set n
, allNodes :: Set n
}
computeNodes :: (Ord n) => Graph n n e -> Nodes n
computeNodes g = Nodes srcs tgts (srcs `Set.union` tgts)
where srcs = sourceNodes g
tgts = targetNodes g
nodes :: (Ord n) => Graph n n e -> Set n
nodes = allNodes . computeNodes
fromNodes :: Ord n => [n] -> Graph n n e
fromNodes ns = Graph $ Map.fromList $ map (, Map.empty) ns
fromList :: (Ord s, Ord t) => [Edge s t e] -> Graph s t e
fromList = fromListWith $ \ new old -> new
fromListWith :: (Ord s, Ord t) => (e -> e -> e) -> [Edge s t e] -> Graph s t e
fromListWith f = List.foldl' (flip (insertEdgeWith f)) empty
toList :: Graph s t e -> [Edge s t e]
toList (Graph g) = [ Edge s t a | (s,m) <- Map.assocs g, (t,a) <- Map.assocs m ]
discrete :: Null e => Graph s t e -> Bool
discrete = all' (all' null) . graph
where all' p = List.all p . Map.elems
clean :: Null e => Graph s t e -> Graph s t e
clean = Graph . filt . fmap filt . graph
where
filt :: Null a => Map k a -> Map k a
filt = Map.filter (not . null)
empty :: Graph s t e
empty = Graph Map.empty
singleton :: s -> t -> e -> Graph s t e
singleton s t e = Graph $ Map.singleton s (Map.singleton t e)
insert :: (Ord s, Ord t) => s -> t -> e -> Graph s t e -> Graph s t e
insert = insertWith $ \ new old -> new
insertEdge :: (Ord s, Ord t) => Edge s t e -> Graph s t e -> Graph s t e
insertEdge (Edge s t e) = insert s t e
insertWith :: (Ord s, Ord t) =>
(e -> e -> e) -> s -> t -> e -> Graph s t e -> Graph s t e
insertWith f s t e (Graph g) = Graph (Map.alter (Just . ins) s g)
where ins Nothing = Map.singleton t e
ins (Just m) = Map.insertWith f t e m
insertEdgeWith :: (Ord s, Ord t) =>
(e -> e -> e) -> Edge s t e -> Graph s t e -> Graph s t e
insertEdgeWith f (Edge s t e) = insertWith f s t e
union :: (Ord s, Ord t) => Graph s t e -> Graph s t e -> Graph s t e
union = unionWith $ \ left right -> left
unionWith :: (Ord s, Ord t) =>
(e -> e -> e) -> Graph s t e -> Graph s t e -> Graph s t e
unionWith f (Graph g) (Graph g') = Graph $ Map.unionWith (Map.unionWith f) g g'
unions ::(Ord s, Ord t) => [Graph s t e] -> Graph s t e
unions = unionsWith $ \ left right -> left
unionsWith :: (Ord s, Ord t) => (e -> e -> e) -> [Graph s t e] -> Graph s t e
unionsWith f = List.foldl' (unionWith f) empty
transpose :: (Ord s, Ord t) => Graph s t e -> Graph t s e
transpose = fromList . map transposeEdge . edges
discardEmpty :: Map k v -> Maybe (Map k v)
discardEmpty m = if Map.null m then Nothing else Just m
removeSourceNode :: Ord s => s -> Graph s t e -> Graph s t e
removeSourceNode s (Graph g) = Graph $ Map.delete s g
removeTargetNode :: Ord t => t -> Graph s t e -> Graph s t e
removeTargetNode t (Graph g) = Graph $ Map.mapMaybe rem g
where rem = discardEmpty . Map.delete t
removeNode :: Ord n => n -> Graph n n e -> Graph n n e
removeNode n = removeTargetNode n . removeSourceNode n
removeEdge :: (Ord s, Ord t) => s -> t -> Graph s t e -> Graph s t e
removeEdge s t (Graph g) = Graph $ Map.adjust (Map.delete t) s g
filterEdges :: (e -> Bool) -> Graph s t e -> Graph s t e
filterEdges f (Graph g) = Graph $ Map.mapMaybe (discardEmpty . Map.filter f) g
unzip :: Graph s t (e, e') -> (Graph s t e, Graph s t e')
unzip g = (fst <$> g, snd <$> g)
mapWithEdge :: (Edge s t e -> e') -> Graph s t e -> Graph s t e'
mapWithEdge f (Graph g) = Graph $ flip Map.mapWithKey g $ \ s m ->
flip Map.mapWithKey m $ \ t e -> f (Edge s t e)
sccs' :: Ord n => Graph n n e -> [Graph.SCC n]
sccs' g =
Graph.stronglyConnComp
[ (n, n, map target (edgesFrom g [n]))
| n <- Set.toList (nodes g)
]
sccs :: Ord n => Graph n n e -> [[n]]
sccs = map Graph.flattenSCC . sccs'
data DAG n = DAG
{ dagGraph :: Graph.Graph
, dagComponentMap :: IntMap (Graph.SCC n)
, dagNodeMap :: Map n Int
}
dagInvariant :: Ord n => DAG n -> Bool
dagInvariant g =
Set.fromList (concatMap Graph.flattenSCC
(IntMap.elems (dagComponentMap g)))
==
Map.keysSet (dagNodeMap g)
&&
IntSet.fromList (Map.elems (dagNodeMap g))
==
IntMap.keysSet (dagComponentMap g)
&&
and [ n `elem` Graph.flattenSCC
(dagComponentMap g IntMap.! (dagNodeMap g Map.! n))
| n <- Map.keys (dagNodeMap g)
]
&&
and [ dagNodeMap g Map.! n == i
| i <- Graph.vertices (dagGraph g)
, n <- Graph.flattenSCC (dagComponentMap g IntMap.! i)
]
&&
IntSet.fromList (Graph.vertices (dagGraph g))
==
IntMap.keysSet (dagComponentMap g)
&&
all isAcyclic (Graph.scc (dagGraph g))
where
isAcyclic (Tree.Node r []) = not (r `elem` (dagGraph g Array.! r))
isAcyclic _ = False
oppositeDAG :: DAG n -> DAG n
oppositeDAG g = g { dagGraph = Graph.transposeG (dagGraph g) }
reachable :: Ord n => DAG n -> Graph.SCC n -> [n]
reachable g scc = case scc of
Graph.AcyclicSCC n -> List.delete n (reachable' n)
Graph.CyclicSCC (n : _) -> reachable' n
Graph.CyclicSCC [] -> __IMPOSSIBLE__
where
lookup' g k = case IntMap.lookup k g of
Nothing -> __IMPOSSIBLE__
Just x -> x
lookup'' g k = case Map.lookup k g of
Nothing -> __IMPOSSIBLE__
Just x -> x
reachable' n =
concatMap (Graph.flattenSCC . lookup' (dagComponentMap g)) $
Graph.reachable (dagGraph g) (lookup'' (dagNodeMap g) n)
sccDAG' ::
forall n e. Ord n
=> Graph n n e
-> [Graph.SCC n]
-> DAG n
sccDAG' g sccs = DAG theDAG componentMap secondNodeMap
where
components :: [(Int, Graph.SCC n)]
components = zip [1..] sccs
firstNodeMap :: Map n Int
firstNodeMap = Map.fromList
[ (n, i)
| (i, c) <- components
, n <- Graph.flattenSCC c
]
targets :: Int -> [n] -> [Int]
targets i ns =
IntSet.toList $ IntSet.fromList
[ j
| e <- edgesFrom g ns
, let j = case Map.lookup (target e) firstNodeMap of
Nothing -> __IMPOSSIBLE__
Just j -> j
, j /= i
]
(theDAG, _, toVertex) =
Graph.graphFromEdges
[ (i, i, targets i (Graph.flattenSCC c))
| (i, c) <- components
]
convertInt :: Int -> Graph.Vertex
convertInt i = case toVertex i of
Nothing -> __IMPOSSIBLE__
Just i -> i
componentMap :: IntMap (Graph.SCC n)
componentMap = IntMap.fromList (map (mapFst convertInt) components)
secondNodeMap :: Map n Int
secondNodeMap = fmap convertInt firstNodeMap
sccDAG :: Ord n => Graph n n e -> DAG n
sccDAG g = sccDAG' g (sccs' g)
acyclic :: Ord n => Graph n n e -> Bool
acyclic = all isAcyclic . sccs'
where
isAcyclic Graph.AcyclicSCC{} = True
isAcyclic Graph.CyclicSCC{} = False
reachableFrom :: Ord n => Graph n n e -> n -> Map n (Int, [Edge n n e])
reachableFrom g n = bfs (SQ.singleton (n, BQ.empty)) Map.empty
where
bfs !q !map = case SQ.lview q of
Nothing -> map
Just ((u, p), q) ->
if u `Map.member` map
then bfs q map
else bfs (foldr SQ.rcons q
[ (v, BQ.rcons (Edge u v e) p)
| (v, e) <- neighbours u g
])
(let n = BQ.size p in
n `seq` Map.insert u (n, BQ.toList p) map)
walkSatisfying ::
Ord n =>
(e -> Bool) -> (e -> Bool) ->
Graph n n e -> n -> n -> Maybe [Edge n n e]
walkSatisfying every some g from to =
case
[ (l1 + l2, p1 ++ [e] ++ map transposeEdge (reverse p2))
| e <- everyEdges
, some (label e)
, (l1, p1) <- maybeToList (Map.lookup (source e) fromReaches)
, (l2, p2) <- maybeToList (Map.lookup (target e) reachesTo)
] of
[] -> Nothing
ess -> Just $ snd $ List.minimumBy (compare `on` fst) ess
where
everyEdges = [ e | e <- toList g, every (label e) ]
fromReaches = reachableFrom (fromList everyEdges) from
reachesTo =
reachableFrom (fromList (map transposeEdge everyEdges)) to
composeWith :: (Ord t, Ord u) => (c -> d -> e) -> (e -> e -> e) ->
Graph s t c -> Graph t u d -> Graph s u e
composeWith times plus (Graph g) (Graph g') = Graph $
Map.mapMaybe (discardEmpty . comp) g where
comp m = Map.fromListWith plus
[ (u, c `times` d)
| (t, c) <- Map.assocs m
, m' <- maybeToList (Map.lookup t g')
, (u, d) <- Map.assocs m'
]
complete :: (Eq e, Null e, SemiRing e, Ord n) => Graph n n e -> Graph n n e
complete g = repeatWhile (mapFst (not . discrete) . combineNewOld' g) g
where
combineNewOld' new old = unzip $ unionWith comb new' old'
where
new' = (,Null.empty) <$> composeWith otimes oplus new old
old' = (Null.empty,) <$> old
comb (new, _) (_, old) = (if x == old then Null.empty else x, x)
where x = old `oplus` new
completeIter :: (Eq e, Null e, SemiRing e, Ord n) => Graph n n e -> [(Graph n n e, Graph n n e)]
completeIter g = iterWhile (not . discrete) (combineNewOld' g) g
where
combineNewOld' new old = unzip $ unionWith comb new' old'
where
new' = (,Null.empty) <$> composeWith otimes oplus new old
old' = (Null.empty,) <$> old
comb (new, _) (_, old) = (if x == old then Null.empty else x, x)
where x = old `oplus` new
gaussJordanFloydWarshallMcNaughtonYamadaReference ::
forall n e. (Ord n, Eq e, StarSemiRing e) =>
Graph n n e -> Graph n n e
gaussJordanFloydWarshallMcNaughtonYamadaReference g =
toGraph (foldr step initialMatrix nodeIndices)
where
indicesAndNodes = zip [1..] $ Set.toList $ nodes g
nodeMap = Map.fromList $ map swap indicesAndNodes
indexMap = Map.fromList indicesAndNodes
noNodes = Map.size nodeMap
nodeIndices = [1 .. noNodes]
matrixBounds = ((1, 1), (noNodes, noNodes))
initialMatrix :: Array.Array (Int, Int) e
initialMatrix =
Array.accumArray
oplus ozero
matrixBounds
[ ((nodeMap Map.! source e, nodeMap Map.! target e), label e)
| e <- edges g
]
rightStrictPair i !e = (i , e)
step k !m =
Array.array
matrixBounds
[ rightStrictPair
(i, j)
(oplus (m Array.! (i, j))
(otimes (m Array.! (i, k))
(otimes (ostar (m Array.! (k, k)))
(m Array.! (k, j)))))
| i <- nodeIndices, j <- nodeIndices
]
toGraph m =
fromList [ Edge (indexMap Map.! i) (indexMap Map.! j) e
| ((i, j), e) <- Array.assocs m
, e /= ozero
]
gaussJordanFloydWarshallMcNaughtonYamada ::
forall n e. (Ord n, Eq e, StarSemiRing e) =>
Graph n n e -> (Graph n n e, [Graph.SCC n])
gaussJordanFloydWarshallMcNaughtonYamada g =
(loop components g, components)
where
components = sccs' g
forwardDAG = sccDAG' g components
reverseDAG = oppositeDAG forwardDAG
loop :: [Graph.SCC n] -> Graph n n e -> Graph n n e
loop [] !g = g
loop (scc : sccs) g =
loop sccs (foldr step g (Graph.flattenSCC scc))
where
canBeReached = reachable forwardDAG scc
canReach = reachable reverseDAG scc
step :: n -> Graph n n e -> Graph n n e
step k !g =
foldr (insertEdgeWith oplus) g
[ Edge i j e
| i <- canReach
, j <- canBeReached
, let e = otimes (lookup' i k) (starTimes (lookup' k j))
, e /= ozero
]
where
starTimes = otimes (ostar (lookup' k k))
lookup' s t = case lookup s t g of
Nothing -> ozero
Just e -> e