{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Utils.Graph.AdjacencyMap.Unidirectional
(
Graph(..)
, invariant
, Edge(..)
, lookup
, edges
, neighbours, neighboursMap
, edgesFrom
, edgesTo
, diagonal
, nodes, sourceNodes, targetNodes, isolatedNodes
, Nodes(..), computeNodes
, discrete
, acyclic
, fromNodes, fromNodeSet
, fromEdges, fromEdgesWith
, empty
, singleton
, insert, insertWith
, insertEdge, insertEdgeWith
, union, unionWith
, unions, unionsWith
, mapWithEdge
, transposeEdge, transpose
, clean
, removeNode, removeNodes
, removeEdge
, filterEdges
, unzip
, composeWith
, sccs'
, sccs
, DAG(..)
, dagInvariant
, oppositeDAG
, reachable
, sccDAG'
, sccDAG
, reachableFrom, reachableFromSet
, walkSatisfying
, gaussJordanFloydWarshallMcNaughtonYamada
, gaussJordanFloydWarshallMcNaughtonYamadaReference
, complete, completeIter
)
where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), lookup, null, unzip )
#else
import Prelude hiding ( lookup, null, unzip )
#endif
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)
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.Pretty
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 n e = Graph
{ graph :: Map n (Map n e)
}
deriving Eq
instance Functor (Graph n) where
fmap f = Graph . Map.map (Map.map f) . graph
invariant :: Ord n => Graph n e -> Bool
invariant g =
Set.isSubsetOf (targetNodes g) (nodes g)
instance (Ord n, Pretty n, Pretty e) => Pretty (Graph n e) where
pretty g = vcat (concat $ map pretty' (Set.toAscList (nodes g)))
where
pretty' n = case edgesFrom g [n] of
[] -> [pretty n]
es -> map pretty es
instance (Ord n, Show n, Show e) => Show (Graph n e) where
showsPrec _ g =
showString "union (fromEdges " .
shows (edges g) .
showString ") (fromNodes " .
shows (Set.toList (isolatedNodes g)) .
showString ")"
data Edge n e = Edge
{ source :: n
, target :: n
, label :: e
} deriving (Eq, Ord, Functor, Show)
instance (Pretty n, Pretty e) => Pretty (Edge n e) where
pretty (Edge s t e) =
pretty s <+> "--(" <> pretty e <> ")-->" <+> pretty t
lookup :: Ord n => n -> n -> Graph n e -> Maybe e
lookup s t (Graph g) = Map.lookup t =<< Map.lookup s g
edges :: Graph n e -> [Edge n e]
edges (Graph g) =
[ Edge s t e
| (s, tes) <- Map.assocs g
, (t, e) <- Map.assocs tes
]
neighbours :: Ord n => n -> Graph n e -> [(n, e)]
neighbours s = Map.toList . neighboursMap s
neighboursMap :: Ord n => n -> Graph n e -> Map n e
neighboursMap s (Graph g) = fromMaybe Map.empty $ Map.lookup s g
edgesFrom :: Ord n => Graph n e -> [n] -> [Edge n e]
edgesFrom (Graph g) ss =
[ Edge s t e
| s <- ss
, m <- maybeToList $ Map.lookup s g
, (t, e) <- Map.assocs m
]
edgesTo :: Ord n => Graph n e -> [n] -> [Edge n 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 e -> [Edge n e]
diagonal (Graph g) =
[ Edge s s e
| (s, m) <- Map.assocs g
, e <- maybeToList $ Map.lookup s m
]
nodes :: Graph n e -> Set n
nodes = Map.keysSet . graph
sourceNodes :: Graph n e -> Set n
sourceNodes = Map.keysSet . Map.filter (not . Map.null) . graph
targetNodes :: Ord n => Graph n e -> Set n
targetNodes = Set.fromList . map target . edges
data Nodes n = Nodes
{ srcNodes :: Set n
, tgtNodes :: Set n
, allNodes :: Set n
}
computeNodes :: Ord n => Graph n e -> Nodes n
computeNodes g =
Nodes { srcNodes = Set.filter (not . null . flip neighbours g) ns
, tgtNodes = targetNodes g
, allNodes = ns
}
where
ns = nodes g
isolatedNodes :: Ord n => Graph n e -> Set n
isolatedNodes g =
Set.difference (allNodes ns) (Set.union (srcNodes ns) (tgtNodes ns))
where
ns = computeNodes g
discrete :: Null e => Graph n e -> Bool
discrete = all' (all' null) . graph
where all' p = List.all p . Map.elems
acyclic :: Ord n => Graph n e -> Bool
acyclic = all isAcyclic . sccs'
where
isAcyclic Graph.AcyclicSCC{} = True
isAcyclic Graph.CyclicSCC{} = False
fromNodes :: Ord n => [n] -> Graph n e
fromNodes ns = Graph $ Map.fromList $ map (, Map.empty) ns
fromNodeSet :: Ord n => Set n -> Graph n e
fromNodeSet ns = Graph $ Map.fromSet (\_ -> Map.empty) ns
fromEdges :: Ord n => [Edge n e] -> Graph n e
fromEdges = fromEdgesWith $ \ new old -> new
fromEdgesWith :: Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e
fromEdgesWith f = List.foldl' (flip (insertEdgeWith f)) empty
empty :: Graph n e
empty = Graph Map.empty
singleton :: Ord n => n -> n -> e -> Graph n e
singleton s t e = insert s t e empty
insert :: Ord n => n -> n -> e -> Graph n e -> Graph n e
insert = insertWith $ \ new old -> new
insertEdge :: Ord n => Edge n e -> Graph n e -> Graph n e
insertEdge (Edge s t e) = insert s t e
insertWith ::
Ord n => (e -> e -> e) -> n -> n -> e -> Graph n e -> Graph n e
insertWith f s t e (Graph g) =
Graph (Map.alter (Just . insNode) t $ Map.alter (Just . insEdge) s g)
where
insEdge Nothing = Map.singleton t e
insEdge (Just m) = Map.insertWith f t e m
insNode Nothing = Map.empty
insNode (Just m) = m
insertEdgeWith ::
Ord n => (e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
insertEdgeWith f (Edge s t e) = insertWith f s t e
union :: Ord n => Graph n e -> Graph n e -> Graph n e
union = unionWith $ \ left right -> left
unionWith ::
Ord n => (e -> e -> e) -> Graph n e -> Graph n e -> Graph n e
unionWith f (Graph g) (Graph g') =
Graph $ Map.unionWith (Map.unionWith f) g g'
unions :: Ord n => [Graph n e] -> Graph n e
unions = unionsWith $ \ left right -> left
unionsWith :: Ord n => (e -> e -> e) -> [Graph n e] -> Graph n e
unionsWith f = List.foldl' (unionWith f) empty
mapWithEdge :: (Edge n e -> e') -> Graph n e -> Graph n e'
mapWithEdge f (Graph g) = Graph $ flip Map.mapWithKey g $ \ s m ->
flip Map.mapWithKey m $ \ t e -> f (Edge s t e)
transposeEdge :: Edge n e -> Edge n e
transposeEdge (Edge s t e) = Edge t s e
transpose :: Ord n => Graph n e -> Graph n e
transpose g =
fromEdges (map transposeEdge (edges g))
`union`
fromNodeSet (isolatedNodes g)
clean :: Null e => Graph n e -> Graph n e
clean = Graph . Map.map (Map.filter (not . null)) . graph
removeNodes :: Ord n => Set n -> Graph n e -> Graph n e
removeNodes ns (Graph g) = Graph (Map.mapMaybeWithKey remSrc g)
where
remSrc s m
| Set.member s ns = Nothing
| otherwise =
Just (Map.filterWithKey (\t _ -> not (Set.member t ns)) m)
removeNode :: Ord n => n -> Graph n e -> Graph n e
removeNode = removeNodes . Set.singleton
removeEdge :: Ord n => n -> n -> Graph n e -> Graph n e
removeEdge s t (Graph g) = Graph $ Map.adjust (Map.delete t) s g
filterEdges :: (Edge n e -> Bool) -> Graph n e -> Graph n e
filterEdges f =
Graph .
Map.mapWithKey (\s ->
Map.filterWithKey (\t l ->
f (Edge { source = s, target = t, label = l }))) .
graph
unzip :: Graph n (e, e') -> (Graph n e, Graph n e')
unzip g = (fst <$> g, snd <$> g)
composeWith ::
Ord n =>
(c -> d -> e) -> (e -> e -> e) ->
Graph n c -> Graph n d -> Graph n e
composeWith times plus (Graph g) (Graph g') = Graph (Map.map 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'
]
sccs' :: Ord n => Graph 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 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 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 = Map.map convertInt firstNodeMap
sccDAG :: Ord n => Graph n e -> DAG n
sccDAG g = sccDAG' g (sccs' g)
reachableFrom :: Ord n => Graph n e -> n -> Map n (Int, [Edge n e])
reachableFrom g n = reachableFromInternal g (Set.singleton n)
reachableFromSet :: Ord n => Graph n e -> Set n -> Set n
reachableFromSet g ns = Map.keysSet (reachableFromInternal g ns)
reachableFromInternal ::
Ord n => Graph n e -> Set n -> Map n (Int, [Edge n e])
reachableFromInternal g ns =
bfs (SQ.fromList (map (, BQ.empty) (Set.toList ns))) 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 =>
(Edge n e -> Bool) -> (Edge n e -> Bool) ->
Graph n e -> n -> n -> Maybe [Edge n e]
walkSatisfying every some g from to =
case
[ (l1 + l2, p1 ++ [e] ++ map transposeEdge (reverse p2))
| e <- everyEdges
, some 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 <- edges g, every e ]
fromReaches = reachableFrom (fromEdges everyEdges) from
reachesTo =
reachableFrom (fromEdges (map transposeEdge everyEdges)) to
complete :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> Graph 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 e -> [(Graph n e, Graph 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 e -> Graph 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 =
fromEdges [ Edge (indexMap Map.! i) (indexMap Map.! j) e
| ((i, j), e) <- Array.assocs m
, e /= ozero
]
`union`
fromNodeSet (nodes g)
gaussJordanFloydWarshallMcNaughtonYamada ::
forall n e. (Ord n, Eq e, StarSemiRing e) =>
Graph n e -> (Graph 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 e -> Graph 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 e -> Graph 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