Agda-2.3.2.1: A dependently typed functional programming language and proof assistant

Agda.Utils.Graph

Synopsis

# Documentation

newtype Graph n e Source

Constructors

 Graph FieldsunGraph :: 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 -> BoolSource

A structural invariant for the graphs.

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

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

All edges originating in the given nodes.

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

Returns all the nodes in the graph.

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

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

Constructs a completely disconnected graph containing the given nodes.

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

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

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

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

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

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

`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 eSource

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

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

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

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

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

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

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

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

Returns `True` iff the graph is acyclic.

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

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 eSource

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 eSource

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

`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 nSource

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)Source

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

All tests.