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
, composeWith
, complete
, gaussJordanFloydWarshallMcNaughtonYamadaReference
, gaussJordanFloydWarshallMcNaughtonYamada
, findPath
, allPaths
)
where
import Prelude hiding (lookup, unzip, null)
import Control.Applicative hiding (empty)
import Control.Monad
import qualified Data.Array.IArray as Array
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 Test.QuickCheck hiding (label)
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.TestHelpers
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 :: (Ord s, Ord t) => 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, Ord t) => 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 s, 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, Ord t) => s -> Graph s t e -> [(t, e)]
neighbours s (Graph g) = maybe [] Map.assocs $ Map.lookup s g
neighboursMap :: (Ord s, Ord t) => s -> Graph s t e -> Map t e
neighboursMap s (Graph g) = fromMaybe Map.empty $ Map.lookup s g
sourceNodes :: (Ord s, Ord t) => Graph s t e -> Set s
sourceNodes = Map.keysSet . graph
targetNodes :: (Ord s, 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 :: (Ord s, Ord t) => 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 :: (Ord s, Ord t, Null e) => Graph s t e -> Graph s t e
clean = Graph . filt . fmap filt . graph
where
filt :: (Ord k, Null a) => Map k a -> Map k a
filt = Map.fromAscList . List.filter (not . null . snd) . Map.toAscList
empty :: Graph s t e
empty = Graph Map.empty
singleton :: (Ord s, Ord t) => 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 s, 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 :: (Ord s, Ord t) => (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 :: (Ord s, Ord t) => (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
composeWith :: (Ord s, 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
gaussJordanFloydWarshallMcNaughtonYamada g = loop components g
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
findPath :: (SemiRing e, Ord n) => (e -> Bool) -> n -> n -> Graph n n e -> Maybe e
findPath good a b g = headMaybe $ filter good $ allPaths good a b g
allPaths :: (SemiRing e, Ord n, Ord c) => (e -> c) -> n -> n -> Graph n n e -> [e]
allPaths classify s t g = paths Set.empty s
where
paths visited s = do
(s', e) <- neighbours s g
let tag = (s', classify e)
recurse = map (e `otimes`) (paths (Set.insert tag visited) s')
if tag `Set.member` visited then []
else if s' == t then e : recurse
else recurse
allTrails :: forall e n. (SemiRing e, Ord n) =>
n -> n -> Graph n n e -> [e]
allTrails s t g = paths Set.empty s
where
paths :: Set (n, n) -> n -> [e]
paths traversed s = do
(s', e) <- neighbours s g
let edge = (s, s')
recurse = (e `otimes`) <$> paths (Set.insert edge traversed) s'
if edge `Set.member` traversed then []
else if s' == t then e : recurse
else recurse
instance (Arbitrary s, Arbitrary t, Arbitrary e) => Arbitrary (Edge s t e) where
arbitrary = Edge <$> arbitrary <*> arbitrary <*> arbitrary
instance (CoArbitrary s, CoArbitrary t, CoArbitrary e) => CoArbitrary (Edge s t e) where
coarbitrary (Edge s t e) = coarbitrary s . coarbitrary t . coarbitrary e
instance (Ord n, SemiRing e, Arbitrary n, Arbitrary e) =>
Arbitrary (Graph n n e) where
arbitrary = do
nodes <- sized $ \ n -> resize (2 * isqrt n) arbitrary
edges <- mapM (\ (n1, n2) -> Edge n1 n2 <$> arbitrary) =<<
listOfElements ((,) <$> nodes <*> nodes)
let g1 = fromList edges
g2 = g1 `union` fromNodes nodes
elements [ g1
, g2
]
where
isqrt :: Int -> Int
isqrt = round . sqrt . fromIntegral
shrink g =
[ removeNode n g | n <- Set.toList $ nodes g ] ++
[ removeEdge n1 n2 g | Edge n1 n2 _ <- edges g ]