Data.Graph.Indexed.Ring.Systems

Computes the ring systems (biconnected components) of
a graph and provides an efficient mapping assigning
each node to the ring system it belongs to.

Definitions

record RingSystems : Nat -> Type -> Type -> Type

  Organizes a graph into a system of biconnected components,
  allowing us to figure out if a node or edge is cyclic,
  as well as get the cyclic subgraph each node or edge
  belongs to.
  
  All lookup functions operate in constant time.

Totality: total
Visibility: public export
Constructor: 

RS : IGraph k e n -> (systems : Nat) -> IArray systems (Subgraph k e n) -> IArray k (Fin (S systems)) -> RingSystems k e n

Projections:

.graph : RingSystems k e n -> IGraph k e n

.ringMap : ({rec:0} : RingSystems k e n) -> IArray k (Fin (S (systems {rec:0})))

.rings : ({rec:0} : RingSystems k e n) -> IArray (systems {rec:0}) (Subgraph k e n)

.systems : RingSystems k e n -> Nat

.graph : RingSystems k e n -> IGraph k e n

Totality: total
Visibility: public export

graph : RingSystems k e n -> IGraph k e n

Totality: total
Visibility: public export

.systems : RingSystems k e n -> Nat

Totality: total
Visibility: public export

systems : RingSystems k e n -> Nat

Totality: total
Visibility: public export

.rings : ({rec:0} : RingSystems k e n) -> IArray (systems {rec:0}) (Subgraph k e n)

Totality: total
Visibility: public export

rings : ({rec:0} : RingSystems k e n) -> IArray (systems {rec:0}) (Subgraph k e n)

Totality: total
Visibility: public export

.ringMap : ({rec:0} : RingSystems k e n) -> IArray k (Fin (S (systems {rec:0})))

Totality: total
Visibility: public export

ringMap : ({rec:0} : RingSystems k e n) -> IArray k (Fin (S (systems {rec:0})))

Totality: total
Visibility: public export

isInRing : RingSystems k e n -> Fin k -> Bool

  True, if the given node is part of a ring systems.

Totality: total
Visibility: export

inSameRing : RingSystems k e n -> Fin k -> Fin k -> Bool

  True, if the two nodes are part of the same ring system.

Totality: total
Visibility: export

ringFor : RingSystems k e n -> Fin k -> Maybe (Subgraph k e n)

  Returns the cyclic subgraph a node belongs to.
  
  Returns `Nothing` if a node is not part of a cycle.

Totality: total
Visibility: export

ringSystems : IGraph k e n -> RingSystems k e n

  Computes the biconnected components and corresponding node mappings
  from an indexed graph.

Totality: total
Visibility: export