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

Safe Haskell | None

Agda.Utils.Graph

Synopsis

- newtype Graph n e = Graph {
  - unGraph :: Map n (Map n e)
  }
- invariant :: Ord n => Graph n e -> Bool
- edges :: Ord n => Graph n e -> [(n, n, e)]
- edgesFrom :: Ord n => Graph n e -> [n] -> [(n, n, e)]
- nodes :: Ord n => Graph n e -> Set n
- filterEdges :: Ord n => (e -> Bool) -> Graph n e -> Graph n e
- fromNodes :: Ord n => [n] -> Graph n e
- 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
- removeEdge :: Ord n => n -> n -> Graph n e -> Graph n e
- 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]
- sccs :: Ord n => Graph n e -> [[n]]
- acyclic :: Ord n => Graph n e -> Bool
- transitiveClosure1 :: (Eq e, SemiRing e, Ord n) => Graph n e -> Graph n e
- transitiveClosure :: (Eq e, SemiRing e, Ord n) => Graph n e -> Graph n e
- 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]
- nodeIn :: (Ord n, Arbitrary n) => Graph n e -> Gen n
- edgeIn :: (Ord n, Arbitrary n, Arbitrary e) => Graph n e -> Gen (n, n, e)
- tests :: IO Bool

# 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.