
  0 | ||| Computes the ring systems (biconnected components) of
  1 | ||| a graph and provides an efficient mapping assigning
  2 | ||| each node to the ring system it belongs to.
  3 | module Data.Graph.Indexed.Ring.Systems
  4 | 
  5 | import Data.Array
  6 | import Data.Graph.Indexed
  7 | import Data.Graph.Indexed.Subgraph
  8 | import Data.Linear.Traverse1
  9 | 
 10 | %default total
 11 | 
 12 | ||| Organizes a graph into a system of biconnected components,
 13 | ||| allowing us to figure out if a node or edge is cyclic,
 14 | ||| as well as get the cyclic subgraph each node or edge
 15 | ||| belongs to.
 16 | |||
 17 | ||| All lookup functions operate in constant time.
 18 | public export
 19 | record RingSystems (k : Nat) (e,n : Type) where
 20 |   constructor RS
 21 |   graph   : IGraph k e n
 22 |   systems : Nat
 23 |   rings   : IArray systems (Subgraph k e n)
 24 |   ringMap : IArray k (Fin (S systems))
 25 | 
 26 | ||| True, if the given node is part of a ring systems.
 27 | export
 28 | isInRing : RingSystems k e n -> Fin k -> Bool
 29 | isInRing rs x =
 30 |   case rs.ringMap `at` x of
 31 |     FZ => False
 32 |     _  => True
 33 | 
 34 | ||| True, if the two nodes are part of the same ring system.
 35 | export
 36 | inSameRing : RingSystems k e n -> (x,y : Fin k) -> Bool
 37 | inSameRing rs x y = isInRing rs x && at rs.ringMap x == at rs.ringMap y
 38 | 
 39 | ||| Returns the cyclic subgraph a node belongs to.
 40 | |||
 41 | ||| Returns `Nothing` if a node is not part of a cycle.
 42 | export
 43 | ringFor : RingSystems k e n -> Fin k -> Maybe (Subgraph k e n)
 44 | ringFor rs x =
 45 |   case rs.ringMap `at` x of
 46 |     FZ   => Nothing
 47 |     FS k => Just $ rs.rings `at` k
 48 | 
 49 | ||| Computes the biconnected components and corresponding node mappings
 50 | ||| from an indexed graph.
 51 | export
 52 | ringSystems : {k : _} -> IGraph k e n -> RingSystems k e n
 53 | ringSystems g =
 54 |  let bcs := biconnectedComponents g
 55 |   in RS g _ (arrayL bcs) (fromPairs k FZ $ zipWithIndex bcs >>= pairs)
 56 | 
 57 |   where
 58 |     pairs : {y : _} -> (Nat,Graph e (Fin k, n)) -> List (Nat, Fin y)
 59 |     pairs (n,G _ g) =
 60 |      let Just x := tryNatToFin (S n) | Nothing => []
 61 |       in (\l => (finToNat $ fst l, x)) <$> labels g
 62 |