module Agda.Utils.Graph.AdjacencyMap.Unidirectional
( Graph(..)
, Edge(..)
, transposeEdge
, edges
, edgesFrom
, edgesTo
, diagonal
, lookup
, neighbours
, sourceNodes, targetNodes
, Nodes(..)
, computeNodes, nodes
, fromNodes
, fromList, fromListWith
, toList
, empty
, singleton
, insert, insertWith
, insertEdge, insertEdgeWith
, union , unionWith
, unions, unionsWith
, removeNode
, removeEdge
, filterEdges
, unzip
, sccs'
, sccs
, acyclic
, composeWith
, transitiveClosure1
, transitiveClosure
, findPath
, allPaths
, nodeIn
, edgeIn
, tests
)
where
import Prelude hiding (lookup, unzip)
import Control.Applicative ((<$>), (<*>))
import Data.Function
import qualified Data.Graph as Graph
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Maybe as Maybe
import Data.Maybe (maybeToList)
import qualified Data.Set as Set
import Data.Set (Set)
import Agda.Utils.Function (iterateUntil)
import Agda.Utils.Functor (for)
import Agda.Utils.List (headMaybe)
import Agda.Utils.QuickCheck as QuickCheck
import Agda.Utils.SemiRing
import Agda.Utils.TestHelpers
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
prop_neighbours :: (Ord s, Ord t, Eq e) => s -> Graph s t e -> Bool
prop_neighbours s g =
neighbours s g == map (\ (Edge s t e) -> (t, e)) (edgesFrom g [s])
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
prop_nodes_fromNodes :: Ord n => [n] -> Bool
prop_nodes_fromNodes ns = sourceNodes (fromNodes ns) == Set.fromList 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 ]
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
prop_insertWith :: (Eq e, Ord s, Ord t) =>
(e -> e -> e) -> s -> t -> e -> Graph s t e -> Bool
prop_insertWith f s t e g =
insertWith f s t e g == unionWith (flip f) g (singleton s t e)
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)
sccs' :: Ord n => Graph n n e -> [Graph.SCC n]
sccs' (Graph g) =
Graph.stronglyConnComp [ (n, n, Map.keys m) | (n, m) <- Map.assocs g ]
sccs :: Ord n => Graph n n e -> [[n]]
sccs = map Graph.flattenSCC . sccs'
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'
]
transitiveClosure1 :: (Eq e, SemiRing e, Ord n) =>
Graph n n e -> Graph n n e
transitiveClosure1 = completeUntilWith (==) otimes oplus
completeUntilWith :: (Ord n) => (Graph n n e -> Graph n n e -> Bool) ->
(e -> e -> e) -> (e -> e -> e) -> Graph n n e -> Graph n n e
completeUntilWith done otimes oplus = iterateUntil done growGraph where
growGraph g = List.foldl' (unionWith oplus) g $ for (edges g) $ \ (Edge s t e) ->
case Map.lookup t (graph g) of
Just es -> Graph $ Map.singleton s $ Map.map (otimes e) es
Nothing -> empty
transitiveClosure :: (Eq e, SemiRing e, Ord n) => Graph n n e -> Graph n n e
transitiveClosure g = List.foldl' extend g $ sccs' g
where
extend g (Graph.AcyclicSCC scc) = fst $ growGraph [scc] (edgesFrom' [scc] g)
extend g (Graph.CyclicSCC scc) = fst $
iterateUntil ((==) `on` snd) (growGraph scc) (edgesFrom' scc g)
edgesFrom' ns g = (g, edgesFrom g ns)
growGraph scc (g, es) = edgesFrom' scc $
List.foldl' (unionWith oplus) g $ for es $ \ (Edge s t e) ->
case Map.lookup t (graph g) of
Just es -> Graph $ Map.singleton s $ Map.map (e `otimes`) es
Nothing -> empty
prop_transitiveClosure :: (Eq e, SemiRing e, Ord n) => Graph n n e -> Property
prop_transitiveClosure g = QuickCheck.label sccInfo $
transitiveClosure g == transitiveClosure1 g
where
sccInfo =
(if noSCCs <= 3 then " " ++ show noSCCs
else ">= 4") ++
" strongly connected component(s)"
where noSCCs = length (sccs g)
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
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 (isqrt n) arbitrary
edges <- mapM (\ (n1, n2) -> Edge n1 n2 <$> arbitrary) =<<
listOfElements ((,) <$> nodes <*> nodes)
return (fromList edges `union` fromNodes nodes)
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 ]
nodeIn :: (Ord n, Arbitrary n) => Graph n n e -> Gen n
nodeIn g = elementsUnlessEmpty (Set.toList $ nodes g)
edgeIn :: (Ord n, Arbitrary n, Arbitrary e) =>
Graph n n e -> Gen (Edge n n e)
edgeIn g = elementsUnlessEmpty (edges g)
type G = Graph N N E
newtype N = N (Positive Int)
deriving (Arbitrary, Eq, Ord)
n :: Int -> N
n = N . Positive
instance Show N where
show (N (Positive n)) = "n " ++ show n
newtype E = E Bool
deriving (Arbitrary, Eq, Show)
instance SemiRing E where
oplus (E x) (E y) = E (x || y)
otimes (E x) (E y) = E (x && y)
tests :: IO Bool
tests = runTests "Agda.Utils.Graph.AdjacencyMap.Unidirectional"
[ quickCheck' (prop_nodes_fromNodes :: [Int] -> Bool)
, quickCheck' (prop_transitiveClosure :: G -> Property)
]