Idris2Doc : Data.Graph.Util

Data.Graph.Util

(source)
Core and utility functionality for graphs

Definitions

match : Node -> Graph e n -> Decomp e n
  Decompose a `Graph` into the `Context` found
for the given node and the remaining `Graph`.

All edges leading to `node` will be removed from the
resulting `Graph`.

Totality: total
Visibility: export
matchAny : Graph e n -> Decomp e n
  Decompose a graph into the `Context` for the largest `Node`
and the remaining `Graph`.

Totality: total
Visibility: export
isEmpty : Graph e n -> Bool
  True, if the given graph is empty

Totality: total
Visibility: export
contexts : Graph e n -> List (Context e n)
  A list of contexts of a graph

Totality: total
Visibility: export
labNodes : Graph e n -> List (LNode n)
  A list of all labeled nodes of a `Graph`

Totality: total
Visibility: export
lab : Graph e n -> Node -> Maybe n
  Find the label for a `Node`.

Totality: total
Visibility: export
elab : Graph e n -> Node -> Node -> Maybe e
  Find the label for an `Edge`.

Totality: total
Visibility: export
nodes : Graph e n -> List Node
  List all 'Node's in the 'Graph'.

Totality: total
Visibility: export
gelem : Node -> Graph e n -> Bool
  `True` if the `Node` is present in the `Graph`.

Totality: total
Visibility: export
order : Graph e n -> Nat
  The number of `Node`s in a `Graph`.

Totality: total
Visibility: export
labEdges : Graph e n -> List (LEdge e)
  A list of all `LEdge`s in the `Graph` (in lexicographic order).

Totality: total
Visibility: export
edges : Graph e n -> List Edge
  List all 'Edge's in the 'Graph'.

Totality: total
Visibility: export
size : Graph e n -> Nat
  The number of edges in the graph.

Totality: total
Visibility: export
lneighbours : Graph e n -> Node -> List (Node, e)
  Find the labelled links to a `Node`.

Totality: total
Visibility: export
neighbourLabels : Graph e n -> Node -> List (n, e)
  Return the labels of all neighbours of a node paired
with the label of the edges leading to those neighbours.

Totality: total
Visibility: export
neighbours : Graph e n -> Node -> List Node
  Find the neighbours for a 'Node'.

Totality: total
Visibility: export
deg : Graph e n -> Node -> Nat
  The degree of the `Node`.

Totality: total
Visibility: export
hasNeighbour : Graph e n -> Node -> Node -> Bool
  Checks if there is an undirected edge between two nodes.

Totality: total
Visibility: export
hasEdge : Graph e n -> Edge -> Bool
  Checks if there is an edge between two nodes.

Totality: total
Visibility: export
hasLEdge : Eq e => Graph e n -> LEdge e -> Bool
  Checks if there is a labelled edge between two nodes.

Totality: total
Visibility: export
add : Context e n -> Graph e n -> Graph e n
  Merge the `Context` into the `DynGraph`.

Context adjacencies should only refer to either a Node already
in a graph.

Behaviour is undefined if the specified 'Node' already exists
in the graph.

Totality: total
Visibility: export
ufold : (Context e n -> c -> c) -> c -> Graph e n -> c
  Fold a function over the graph by recursively calling 'match'.

Totality: total
Visibility: export
gmap : (Context e1 n1 -> Context e2 n2) -> Graph e1 n1 -> Graph e2 n2
  Map a function over the graph by recursively calling `match`.

Totality: total
Visibility: export
insNode : Node -> n -> Graph e n -> Graph e n
  Insert a labeled node into the `Graph`.
The behavior is undefined if the node is already
in the graph.

Totality: total
Visibility: export
insEdge : LEdge e -> Graph e n -> Graph e n
  Insert a `LEdge` into the 'Graph'.
Behavior is undefined if the edge does not
connect two nodes already in the graph.

Totality: total
Visibility: export
insNodes : List (LNode n) -> Graph e n -> Graph e n
  Insert multiple `LNode`s into the `Graph`.

Totality: total
Visibility: export
insEdges : List (LEdge e) -> Graph e n -> Graph e n
  Insert multiple `LEdge`s into the `Graph`.

Totality: total
Visibility: export
delNode : Node -> Graph e n -> Graph e n
  Remove a 'Node' from the 'Graph'.

Totality: total
Visibility: export
delNodes : List Node -> Graph e n -> Graph e n
  Remove multiple 'Node's from the 'Graph'.

Totality: total
Visibility: export
delEdge : Edge -> Graph e n -> Graph e n
  Remove an 'Edge' from the 'Graph'.

Totality: total
Visibility: export
delEdges : List Edge -> Graph e n -> Graph e n
  Remove multiple 'Edge's from the 'Graph'.

Totality: total
Visibility: export
labnfilter : (LNode n -> Bool) -> Graph e n -> Graph e n
  Returns the subgraph only containing the labelled nodes which
satisfy the given predicate.

Totality: total
Visibility: export
nfilter : (Node -> Bool) -> Graph e n -> Graph e n
  Returns the subgraph only containing the nodes which satisfy the
given predicate.

Totality: total
Visibility: export
labfilter : (n -> Bool) -> Graph e n -> Graph e n
  Returns the subgraph only containing the nodes whose labels
satisfy the given predicate.

Totality: total
Visibility: export
pairWithNeighbours : Graph e n -> Graph e (n, List (n, e))
  Retruns the same graph additionaly containing list of connecting
edges and labels to each node.

Totality: total
Visibility: export
pairWithNeighbours' : Graph e n -> Graph e (n, List n)
  Returns the same graph additionaly containing list of connecting
labels to each node.

Totality: total
Visibility: export
empty : Graph e n
  An empty `Graph`

Totality: total
Visibility: export
mkGraph : List (LNode n) -> List (LEdge e) -> Graph e n
  Create a `Graph` from the list of labeled nodes and
edges.

TODO: Can we easily enforce that the edges only point
To the nodes in the list?

Totality: total
Visibility: export
pretty : (e -> String) -> (n -> String) -> Graph e n -> String
Totality: total
Visibility: export