Agda.Utils.Graph

Documentation

newtype Graph n e

Constructors

Graph

Fields

unGraph :: Map n (Map n e)

Instances

Functor (Graph n)

(Eq n, Eq e) => Eq (Graph n e)

(Show n, Show e) => Show (Graph n e)

(Ord n, SemiRing e, Arbitrary n, Arbitrary e) => Arbitrary (Graph n e)

(PrettyTCM n, PrettyTCM (n, e)) => PrettyTCM (Graph n e)

invariant :: Ord n => Graph n e -> Bool

A structural invariant for the graphs.

edges :: Ord n => Graph n e -> [(n, n, e)]

edgesFrom :: Ord n => Graph n e -> [n] -> [(n, n, e)]

All edges originating in the given nodes.

nodes :: Ord n => Graph n e -> Set n

Returns all the nodes in the graph.

filterEdges :: Ord n => (e -> Bool) -> Graph n e -> Graph n e

fromNodes :: Ord n => [n] -> Graph n e

Constructs a completely disconnected graph containing the given nodes.

fromList :: (SemiRing e, Ord n) => [(n, n, e)] -> Graph n e

empty :: Graph n e

singleton :: Ord n => n -> n -> e -> Graph n e

insert :: (SemiRing e, Ord n) => n -> n -> e -> Graph n e -> Graph n e

removeNode :: Ord n => n -> Graph n e -> Graph n e

Removes the given node, and all corresponding edges, from the graph.

removeEdge :: Ord n => n -> n -> Graph n e -> Graph n e

removeEdge n1 n2 g removes the edge going from n1 to n2, if any.

union :: (SemiRing e, Ord n) => Graph n e -> Graph n e -> Graph n e

unions :: (SemiRing e, Ord n) => [Graph n e] -> Graph n e

lookup :: Ord n => n -> n -> Graph n e -> Maybe e

neighbours :: Ord n => n -> Graph n e -> [(n, e)]

sccs' :: Ord n => Graph n e -> [SCC n]

The graph's strongly connected components, in reverse topological order.

sccs :: Ord n => Graph n e -> [[n]]

The graph's strongly connected components, in reverse topological order.

acyclic :: Ord n => Graph n e -> Bool

Returns True iff the graph is acyclic.

transitiveClosure1 :: (Eq e, SemiRing e, Ord n) => Graph n e -> Graph n e

Computes the transitive closure of the graph.

Note that this algorithm is not guaranteed to be correct (or terminate) for arbitrary semirings.

This function operates on the entire graph at once.

transitiveClosure :: (Eq e, SemiRing e, Ord n) => Graph n e -> Graph n e

Computes the transitive closure of the graph.

Note that this algorithm is not guaranteed to be correct (or terminate) for arbitrary semirings.

This function operates on one strongly connected component at a time.

findPath :: (SemiRing e, Ord n) => (e -> Bool) -> n -> n -> Graph n e -> Maybe e

allPaths :: (SemiRing e, Ord n, Ord c) => (e -> c) -> n -> n -> Graph n e -> [e]

allPaths classify a b g returns a list of pathes (accumulated edge weights) from node a to node b in g. Alternative intermediate pathes are only considered if they are distinguished by the classify function.

nodeIn :: (Ord n, Arbitrary n) => Graph n e -> Gen n

Generates a node from the graph. (Unless the graph is empty.)

edgeIn :: (Ord n, Arbitrary n, Arbitrary e) => Graph n e -> Gen (n, n, e)

Generates an edge from the graph. (Unless the graph contains no edges.)

tests :: IO Bool

All tests.