Idris2Doc : Data.Graph.Indexed.Util

Data.Graph.Indexed.Util

(source)
Definitions
lupdNodes : MArray s k (Adj k e n) -> (n -> n) -> F1' s
  Updates all node labels in a mutable graph.

  Totality: total
  Visibility: export
lupdNode : MArray s k (Adj k e n) -> Fin k -> (n -> n) -> F1' s
  Updates the node label at the given position in a mutable graph.

  Totality: total
  Visibility: export
lsetNode : MArray s k (Adj k e n) -> Fin k -> n -> F1' s
  Sets the node label at the given position in a mutable graph.

  Totality: total
  Visibility: export
linsEdge : MArray s k (Adj k e n) -> Edge k e -> F1' s
  Insert a single edge into a mutable array-representation of a graph.

  Totality: total
  Visibility: export
ldelEdge : MArray s k (Adj k e n) -> Fin k -> Fin k -> F1' s
  Delete a single edge from a mutable array-representation of a graph.

  Totality: total
  Visibility: export
linsEdges : MArray s k (Adj k e n) -> List (Edge k e) -> F1' s
  Insert a bunch of edges into a mutable array-representation of a graph.

  Totality: total
  Visibility: export
ldelEdges : MArray s k (Adj k e n) -> List (Fin k, Fin k) -> F1' s
  Insert a bunch of edges into a mutable array-representation of a graph.

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

  Totality: total
  Visibility: export
nodes : (0 _ : IGraph k e n) -> List (Fin k)
  List all 'Node's in the 'Graph'.

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

  Totality: total
  Visibility: export
labels : IGraph k e n -> List n
  A list of all labeled nodes of a `Graph`

  Totality: total
  Visibility: export
adj : IGraph k e n -> Fin k -> Adj k e n
  Returns the adjacency (node label plus labeled edges to neighbours)
  of a node in a graph.

  Totality: total
  Visibility: export
lab : IGraph k e n -> Fin k -> n
  Returns the label of a node in graph.

  Totality: total
  Visibility: export
neighboursAsAL : IGraph k e n -> Fin k -> AssocList k e
  Returns the edges connecting a node as an `AssocList`
  (nodes plus edge labels).

  Totality: total
  Visibility: export
neighboursAsPairs : IGraph k e n -> Fin k -> List (Fin k, e)
  Returns the edges connecting a node as a list of pairs
  (nodes plus edge labels).

  Totality: total
  Visibility: export
neighbours : IGraph k e n -> Fin k -> List (Fin k)
  Returns the list of neighbouring nodes of a node in a graph.

  Totality: total
  Visibility: export
edgesTo : IGraph k e n -> Fin k -> List (Edge k e)
  Returns the list of edges connecting a node.

  Totality: total
  Visibility: export
lneighbours : IGraph k e n -> Fin k -> List (Fin k, n)
  Returns the list of neighboring nodes paired with their
  corresponding labels.

  Totality: total
  Visibility: export
lneighboursAsAL : IGraph k e n -> Fin k -> AssocList k (e, n)
  Returns the edges connecting a node paired with the
  neighbouring node labels.

  Totality: total
  Visibility: export
neighbourLabels : IGraph k e n -> Fin k -> List n
  Returns the labels of neighbour nodes of a node.

  Totality: total
  Visibility: export
edgeLabels : IGraph k e n -> Fin k -> List e
  Returns the labels of edges connecting a node.

  Totality: total
  Visibility: export
elab : IGraph k e n -> Fin k -> Fin k -> Maybe e
  Find the label for an `Edge`.

  Totality: total
  Visibility: export
edge : IGraph k e n -> Fin k -> Fin k -> Maybe (Edge k e)
  Find the label for an `Edge`.

  Totality: total
  Visibility: export
adjacent : IGraph k e n -> Fin k -> Fin k -> Bool
  Tests if the given nodes are adjecent (connected via an edge).

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

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

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

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

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

  Totality: total
  Visibility: export
mkGraphL : (ns : List n) -> List (Edge (length ns) e) -> IGraph (length ns) e n
  Create a `Graph` from a list of labeled nodes and edges.

  Totality: total
  Visibility: export
mkGraph : Vect k n -> List (Edge k e) -> IGraph k e n
  Create a `Graph` from a vect of labeled nodes and edges.

  Totality: total
  Visibility: export
mkGraphRev : Vect k n -> List (Edge k e) -> IGraph k e n
  Create a `Graph` from a vect of labeled nodes and edges.
  
  Unlike `mkGraph`, this puts the nodes in the array in reverse order,
  which is useful when they come from a parser with the last node being
  at the head of the vector.

  Totality: total
  Visibility: export
generate : (k : Nat) -> (Fin k -> Adj k e n) -> IGraph k e n
  Totality: total
  Visibility: export
mapCtxt : (Fin k -> Adj k e n -> Adj k e1 n1) -> IGraph k e n -> IGraph k e1 n1
  Map the adjacencies in a graph accoring to each node's context

  Totality: total
  Visibility: export
mapWithCtxt : (Fin k -> Adj k e n -> n1) -> IGraph k e n -> IGraph k e n1
  Map the node labels in a graph accoring to each node's context

  Totality: total
  Visibility: export
mapAdj : (Adj k e n -> Adj k f m) -> IGraph k e n -> IGraph k f m
  Map the adjacencies in a graph

  Totality: total
  Visibility: export
mapWithAdj : (Adj k e n -> m) -> IGraph k e n -> IGraph k e m
  Map the node labels in a graph accoring to each node's adjacency

  Totality: total
  Visibility: export
traverseCtxt : Applicative f => (Fin k -> Adj k e n -> f (Adj k e1 n1)) -> IGraph k e n -> f (IGraph k e1 n1)
  Totality: total
  Visibility: export
traverseWithCtxt : Applicative f => (Fin k -> Adj k e n -> f n1) -> IGraph k e n -> f (IGraph k e n1)
  Totality: total
  Visibility: export
updateNodes : Fin k -> (m -> n) -> (m -> n) -> IGraph k e m -> IGraph k e n
  Uses two functions for updating nodes in a graph:
  
  Once is used for the given node, the other for all other nodes.

  Totality: total
  Visibility: export
updateNode : Fin k -> (n -> n) -> IGraph k e n -> IGraph k e n
  Updates a single node in the graph at the given position.

  Totality: total
  Visibility: export
setNode : Fin k -> n -> IGraph k e n -> IGraph k e n
  Replaces a single node in the graph at the given position.

  Totality: total
  Visibility: export
updateEdges : Fin k -> Fin k -> (e -> e2) -> (e -> e2) -> IGraph k e n -> IGraph k e2 n
  Uses two functions for updating the edge labels in a graph.
  
  Once is used for the edge connecting the two given nodes, the other for
  all other edges.

  Totality: total
  Visibility: export
updateEdge : Fin k -> Fin k -> (e -> e) -> IGraph k e n -> IGraph k e n
  Uses a function for updating a single edge label in a graph.

  Totality: total
  Visibility: export
insEdges : List (Edge k e) -> IGraph k e n -> IGraph k e n
  Insert (or replace) a single edge in a graph.

  Totality: total
  Visibility: export
insEdge : Edge k e -> IGraph k e n -> IGraph k e n
  Insert an `Edge` into the 'IGraph'.

  Totality: total
  Visibility: export
delEdges : List (Fin k, Fin k) -> IGraph k e n -> IGraph k e n
  Remove multiple 'Edge's from the 'Graph'.

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

  Totality: total
  Visibility: export
insNodes : IGraph k e n -> Vect m n -> IGraph (k + m) e n
  Insert multiple `LNode`s into the `Graph`.

  Totality: total
  Visibility: export
insNodesAndEdges : IGraph k e n -> Vect m n -> List (Edge (k + m) e) -> IGraph (k + m) e n
  Insert multiple `LNode`s into the `Graph`.

  Totality: total
  Visibility: export
insNode : IGraph k e n -> n -> IGraph (S k) 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
adjEdges : SortedMap (Fin x) (Fin y) -> Adj x e n -> Adj y e n
  Totality: total
  Visibility: export
delNodes : List (Fin k) -> IGraph k e n -> Graph e n
  Totality: total
  Visibility: export
delNode : Fin k -> IGraph k e n -> Graph e n
  Remove a 'Node' from the 'Graph'.

  Totality: total
  Visibility: export
mergeGraphsWithEdges : IGraph k e n -> IGraph m e n -> List (Fin k, (Fin m, e)) -> IGraph (k + m) e n
  Merge two graphs connecting them via the given list of
  edges

  Totality: total
  Visibility: export
mergeGraphs : IGraph k e n -> IGraph m e n -> IGraph (k + m) e n
  Merge two graphs that have no bonds between them.

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