0 | module Data.Graph.Indexed.Subgraph
  1 |
  2 | import Data.Array
  3 | import Data.Array.Mutable
  4 | import Data.AssocList.Indexed
  5 | import Data.Graph.Indexed.Query.DFS
  6 | import Data.Graph.Indexed.Types
  7 | import Data.Graph.Indexed.Util
  8 | import Data.Linear.Ref1
  9 | import Data.SortedMap
 10 |
 11 | %default total
 12 |
 13 | --------------------------------------------------------------------------------
 14 | -- Utilities
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| A mapping from indices in one array (or graph) to indices in another.
 18 | public export
 19 | 0 NodeMap : (k,m : Nat) -> Type
 20 | NodeMap k m = SortedMap (Fin k) (Fin m)
 21 |
 22 | ||| Computes a node map from an array of indices.
 23 | export %inline
 24 | nodeMap : {k : _} -> IArray k (Fin m) -> NodeMap m k
 25 | nodeMap = foldrKV (flip insert) empty
 26 |
 27 | ||| Adjust an assoc list (a list of edges) according to a mapping from
 28 | ||| old nodes to new nodes.
 29 | export %inline
 30 | adjAssocList : NodeMap k m -> AssocList k e -> AssocList m e
 31 | adjAssocList nm = foldl ins empty . pairs
 32 |   where
 33 |     ins : AssocList m e -> (Fin k,e) -> AssocList m e
 34 |     ins l (x,ve) = maybe l (\y => insert y ve l) (lookup x nm)
 35 |
 36 | --------------------------------------------------------------------------------
 37 | -- Subgraphs
 38 | --------------------------------------------------------------------------------
 39 |
 40 | ||| An indexed graph that represents a subgraph on another one.
 41 | |||
 42 | ||| Every node is linked to the node in the original graph.
 43 | public export
 44 | 0 ISubgraph : (k,m : Nat) -> (e,n : Type) -> Type
 45 | ISubgraph k m e n = IGraph k e (Fin m, n)
 46 |
 47 | ||| An graph that represents a subgraph on another one.
 48 | |||
 49 | ||| Every node is linked to the node in the original graph.
 50 | public export
 51 | 0 Subgraph : (m : Nat) -> (e,n : Type) -> Type
 52 | Subgraph m e n = Graph e (Fin m, n)
 53 |
 54 | ||| Computes a subgraph of a graph containing the given nodes.
 55 | ||| Runs in O(k * log (k)) for sparse graphs.
 56 | export
 57 | subgraph : {k : _} -> IGraph m e n -> IArray k (Fin m) -> ISubgraph k m e n
 58 | subgraph (IG g) arr = let m := nodeMap arr in IG $ map (adj m) arr
 59 |
 60 |   where
 61 |     adj : NodeMap m k -> Fin m -> Adj k e (Fin m, n)
 62 |     adj m fm = let A l ns := at g fm in A (fm,l) (adjAssocList m ns)
 63 |
 64 | ||| Computes a subgraph of a graph containing the given nodes.
 65 | ||| Runs in O(k * log (k)) for sparse graphs.
 66 | export
 67 | subgraphL : IGraph m e n -> List (Fin m) -> Subgraph m e n
 68 | subgraphL g ns = G _ $ subgraph g (arrayL ns)
 69 |
 70 | ||| Extracts the connected components of a potentially disconnected
 71 | ||| graph.
 72 | |||
 73 | ||| Runs in O(k * log(k)) for sparse graphs.
 74 | export
 75 | connectedComponents : {k : _} -> IGraph k e n -> List (Subgraph k e n)
 76 | connectedComponents g = subgraphL g . (<>> []) <$> components g
 77 |
 78 | ||| Converts the node of a subgraph to the corresponding node in the
 79 | ||| original graph.
 80 | export
 81 | origin : ISubgraph k m e n -> Fin k -> Fin m
 82 | origin s = fst . lab s
 83 |
 84 | ||| Converts the edge of a subgraph to the corresponding edge in the
 85 | ||| original graph.
 86 | |||
 87 | ||| This comes with the potential of failure, since we cannot prove that
 88 | ||| the subgraph is injective, that is, distinct nodes in the subgraph
 89 | ||| point at distinct nodes in the original graph.
 90 | export
 91 | originEdge : ISubgraph k m e n -> Edge k e -> Maybe (Edge m e)
 92 | originEdge s (E x y l) = mkEdge (origin s x) (origin s y) l
 93 |
 94 | --------------------------------------------------------------------------------
 95 | -- Biconnected Components
 96 | --------------------------------------------------------------------------------
 97 |
 98 | 0 Stack : Type -> Nat -> Type
 99 | Stack s n = Ref s (List $ Fin n)
100 |
101 | 0 Comps : Type -> Nat -> Type
102 | Comps s n = Ref s (List (List $ Fin n))
103 |
104 | pop : Stack s k -> F1' s
105 | pop s = mod1 s $ \case h::t => t; [] => []
106 |
107 | extractComp : Fin k -> Stack s k -> Comps s k -> F1' s
108 | extractComp n s c t =
109 |   let st # t := read1 s t
110 |       (cmp,rem) := go [<] st
111 |       _ # t     := mod1 c (cmp::) t
112 |    in write1 s rem t
113 |
114 |   where
115 |     go : SnocList (Fin k) -> List (Fin k) -> (List $ Fin k, List $ Fin k)
116 |     go sx (x :: xs) = if n == x then (sx <>> [x], xs) else go (sx :< x) xs
117 |     go sx []        = (sx <>> [], []) -- this should not happen
118 |
119 | parameters (g : IGraph k e n)
120 |            (d : MArray t k Nat)
121 |            (s : Stack t k)
122 |            (c : Comps t k)
123 |     covering sc : Fin k -> Fin k -> Nat -> F1 t Nat
124 |
125 |     covering scs : List (Fin k) -> Fin k -> Nat -> F1 t Nat
126 |     scs []      p dpt t = dpt # t
127 |     scs (x::xs) p dpt t =
128 |       let r2 # t2 := sc x p dpt t
129 |           r3 # t3 := scs xs p dpt t2
130 |        in min r2 r3 # t3
131 |
132 |     sc n p dpt t =
133 |       let Z  # t := get d n t | res => res
134 |           _ # t  := set d n dpt t
135 |           _ # t  := mod1 s (n::) t
136 |           dc # t := scs (filter (/= p) $ neighbours g n) n (S dpt) t
137 |        in case compare dc dpt of
138 |             LT => dc # t
139 |             EQ => let _ # t := extractComp n s c t in dc # t
140 |             GT => let _ # t := Subgraph.pop s t in dpt # t
141 |
142 |     go : List (Fin k) -> F1 t (List $ Subgraph k e n)
143 |     go []      t = mapR1 (map (subgraphL g)) (read1 c t)
144 |     go (n::ns) t =
145 |       let Z # t := get d n t | _ # t => go ns t
146 |           _ # t := assert_total $ sc n n 1 t
147 |        in go ns t
148 |
149 | ||| Extracts the biconnected components of a graph (Hopcroft/Tarjan algorithm).
150 | |||
151 | ||| A graph is "biconnected" or "2-connected" if at least two of
152 | ||| its edges need to be removed to get to a disconnected graph.
153 | |||
154 | ||| Biconnected subgraphs only consist of cyclic vertices and edges.
155 | ||| When analyzing the cycles in a graph, for instance, when computing
156 | ||| the relevant cycles or a minimal cycle basis, it is always sufficient
157 | ||| - and often much more efficient - to inspect the biconnected
158 | ||| components in isolation.
159 | export
160 | biconnectedComponents : {k : _} -> IGraph k e n -> List (Subgraph k e n)
161 | biconnectedComponents g =
162 |   run1 $ \t =>
163 |     let c # t := ref1 (the (List (List $ Fin k)) []) t
164 |         s # t := ref1 (the (List $ Fin k) []) t
165 |         d # t := marray1 k Z t
166 |      in go g d s c (allFinsFast k) t
167 |