Data.Graph.Indexed.Util

Definitions

allFinsFast : (n : Nat) -> List (Fin n)

  Generates the list of all `Fin n` in linear type.
  
  This is a lot faster than `Data.Fin.allFins`, which runs in quadratic
  time.

Totality: total
Visibility: export

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