
   0 | module Data.Graph.Indexed.Util
   1 | 
   2 | import Data.Array
   3 | import Data.Array.Mutable
   4 | import Data.AssocList.Indexed
   5 | import Data.Linear.Traverse1
   6 | import Data.Graph.Indexed.Types
   7 | import Data.SortedMap
   8 | import Data.SortedSet
   9 | import Data.List
  10 | import Data.String
  11 | import Data.Vect
  12 | 
  13 | %default total
  14 | 
  15 | ||| Generates the list of all `Fin n` in linear type.
  16 | |||
  17 | ||| This is a lot faster than `Data.Fin.allFins`, which runs in quadratic
  18 | ||| time.
  19 | export
  20 | allFinsFast : (n : Nat) -> List (Fin n)
  21 | allFinsFast 0 = []
  22 | allFinsFast (S n) = go [] last
  23 |   where
  24 |     go : List (Fin $ S n) -> Fin (S n) -> List (Fin $ S n)
  25 |     go xs FZ     = FZ :: xs
  26 |     go xs (FS x) = go (FS x :: xs) (assert_smaller (FS x) $ weaken x)
  27 | 
  28 | --------------------------------------------------------------------------------
  29 | --          Internal utilities
  30 | --------------------------------------------------------------------------------
  31 | 
  32 | ||| Updates all node labels in a mutable graph.
  33 | export %inline
  34 | lupdNodes : {k : _} -> MArray s k (Adj k e n) -> (n -> n) -> F1' s
  35 | lupdNodes r f = mupdate {label $= f} r
  36 | 
  37 | parameters (r : MArray s k (Adj k e n))
  38 | 
  39 |   ||| Updates the node label at the given position in a mutable graph.
  40 |   export %inline
  41 |   lupdNode : (n1 : Fin k) -> (n -> n) -> F1' s
  42 |   lupdNode n1 f = modify r n1 {label $= f}
  43 | 
  44 |   ||| Sets the node label at the given position in a mutable graph.
  45 |   export %inline
  46 |   lsetNode : (n1 : Fin k) -> n -> F1' s
  47 |   lsetNode n1 v = modify r n1 {label := v}
  48 | 
  49 |   ||| Insert a single edge into a mutable array-representation of a graph.
  50 |   export
  51 |   linsEdge : Edge k e ->F1' s
  52 |   linsEdge (E n1 n2 el) t =
  53 |     let _ # t := modify r n1 {neighbours $= insert n2 el} t
  54 |      in modify r n2 {neighbours $= insert n1 el} t
  55 | 
  56 |   ||| Delete a single edge from a mutable array-representation of a graph.
  57 |   export
  58 |   ldelEdge : (n1, n2 : Fin k) -> F1' s
  59 |   ldelEdge n1 n2 t =
  60 |     let _ # t := modify r n1 {neighbours $= delete n2} t
  61 |      in modify r n2 {neighbours $= delete n1} t
  62 | 
  63 |   ||| Insert a bunch of edges into a mutable array-representation of a graph.
  64 |   export %inline
  65 |   linsEdges : List (Edge k e) -> F1' s
  66 |   linsEdges = traverse1_ linsEdge
  67 | 
  68 |   ||| Insert a bunch of edges into a mutable array-representation of a graph.
  69 |   export %inline
  70 |   ldelEdges : List (Fin k, Fin k) -> F1' s
  71 |   ldelEdges = traverse1_ (\(x,y) => ldelEdge x y)
  72 | 
  73 | -- we return only edges to nodes greater than the node in the
  74 | -- context to avoid returning every edge twice in `labEdges`.
  75 | ctxtEdges : Fin k -> Adj k e n -> SnocList (Edge k e)
  76 | ctxtEdges x (A _ ns) = foldlKV acc [<] ns
  77 | 
  78 |   where
  79 |     acc : Fin k -> SnocList (Edge k e) -> e -> SnocList (Edge k e)
  80 |     acc y sp v with (compare x y) proof eq
  81 |       _ | LT = sp :< E x y v
  82 |       _ | _  = sp
  83 | 
  84 | --------------------------------------------------------------------------------
  85 | --          Inspecting Graphs
  86 | --------------------------------------------------------------------------------
  87 | 
  88 | ||| A list of contexts of a graph
  89 | export
  90 | contexts : {k : _} -> IGraph k e n -> List (Context k e n)
  91 | contexts = foldrKV (\x,(A l ns),cs => C x l ns :: cs) [] . graph
  92 | 
  93 | ||| List all 'Node's in the 'Graph'.
  94 | export %inline
  95 | nodes : {k : _} -> (0 _ : IGraph k e n) -> List (Fin k)
  96 | nodes _ = allFinsFast k
  97 | 
  98 | ||| A list of all labeled nodes of a `Graph`
  99 | export
 100 | labNodes  : {k : _} -> IGraph k e n -> List (Fin k, n)
 101 | labNodes = foldrKV (\x,(A l _),cs => (x,l) :: cs) [] . graph
 102 | 
 103 | ||| A list of all labeled nodes of a `Graph`
 104 | export
 105 | labels  : {k : _} -> IGraph k e n -> List n
 106 | labels = foldr (\(A l _) => (l ::)) [] . graph
 107 | 
 108 | ||| Returns the adjacency (node label plus labeled edges to neighbours)
 109 | ||| of a node in a graph.
 110 | export %inline
 111 | adj : IGraph k e n -> Fin k -> Adj k e n
 112 | adj (IG g) k = at g k
 113 | 
 114 | ||| Returns the label of a node in graph.
 115 | export %inline
 116 | lab : IGraph k e n -> Fin k -> n
 117 | lab g = label . adj g
 118 | 
 119 | ||| Returns the edges connecting a node as an `AssocList`
 120 | ||| (nodes plus edge labels).
 121 | export %inline
 122 | neighboursAsAL : IGraph k e n -> Fin k -> AssocList k e
 123 | neighboursAsAL g = neighbours . adj g
 124 | 
 125 | ||| Returns the edges connecting a node as a list of pairs
 126 | ||| (nodes plus edge labels).
 127 | export %inline
 128 | neighboursAsPairs : IGraph k e n -> Fin k -> List (Fin k, e)
 129 | neighboursAsPairs g = pairs . neighboursAsAL g
 130 | 
 131 | ||| Returns the list of neighbouring nodes of a node in a graph.
 132 | export %inline
 133 | neighbours : IGraph k e n -> Fin k -> List (Fin k)
 134 | neighbours g = keys . neighboursAsAL g
 135 | 
 136 | ||| Returns the list of edges connecting a node.
 137 | export %inline
 138 | edgesTo : IGraph k e n -> Fin k -> List (Edge k e)
 139 | edgesTo g k =
 140 |   let A _ ns := adj g k
 141 |    in mapMaybe (\(n,l) => mkEdge k n l) $ pairs ns
 142 | 
 143 | ||| Returns the list of neighboring nodes paired with their
 144 | ||| corresponding labels.
 145 | export
 146 | lneighbours : IGraph k e n -> Fin k -> List (Fin k, n)
 147 | lneighbours g = map (\x => (x, lab g x)) . neighbours g
 148 | 
 149 | ||| Returns the edges connecting a node paired with the
 150 | ||| neighbouring node labels.
 151 | export
 152 | lneighboursAsAL : IGraph k e n -> Fin k -> AssocList k (e, n)
 153 | lneighboursAsAL g = mapKV (\x => (, lab g x)) . neighboursAsAL g
 154 | 
 155 | ||| Returns the labels of neighbour nodes of a node.
 156 | export
 157 | neighbourLabels : IGraph k e n -> Fin k -> List n
 158 | neighbourLabels g = map (lab g) . neighbours g
 159 | 
 160 | ||| Returns the labels of edges connecting a node.
 161 | export %inline
 162 | edgeLabels : IGraph k e n -> Fin k -> List e
 163 | edgeLabels g = values . neighbours . adj g
 164 | 
 165 | ||| Find the label for an `Edge`.
 166 | export
 167 | elab : IGraph k e n -> Fin k -> Fin k -> Maybe e
 168 | elab (IG g) x y = lookup y . neighbours $ at g x
 169 | 
 170 | ||| Find the label for an `Edge`.
 171 | export
 172 | edge : IGraph k e n -> Fin k -> Fin k -> Maybe (Edge k e)
 173 | edge g x y = elab g x y >>= mkEdge x y
 174 | 
 175 | ||| Tests if the given nodes are adjecent (connected via an edge).
 176 | export
 177 | adjacent : IGraph k e n -> Fin k -> Fin k -> Bool
 178 | adjacent g x y = isJust $ elab g x y
 179 | 
 180 | ||| A list of all `LEdge`s in the `Graph` (in lexicographic order).
 181 | export
 182 | edges  : {k : _} -> IGraph k e n -> List (Edge k e)
 183 | edges (IG g) = foldrKV (\x,adj,es => ctxtEdges x adj <>> es) [] g
 184 | 
 185 | ||| The number of edges in the graph.
 186 | export
 187 | size : {k : _} -> IGraph k e n -> Nat
 188 | size = length . edges
 189 | 
 190 | ||| The degree of the `Node`.
 191 | export
 192 | deg : IGraph k e n -> Fin k -> Nat
 193 | deg g = length . neighbours g
 194 | 
 195 | ||| Checks if there is an undirected edge between two nodes.
 196 | export
 197 | hasNeighbour : IGraph k e n -> Fin k -> Fin k -> Bool
 198 | hasNeighbour g k = isJust . elab g k
 199 | 
 200 | --------------------------------------------------------------------------------
 201 | --          Making Graphs
 202 | --------------------------------------------------------------------------------
 203 | 
 204 | ||| An empty `Graph`
 205 | export
 206 | empty : IGraph 0 e n
 207 | empty = IG empty
 208 | 
 209 | 0 mapLen : (f : a -> b) -> (as : List a) -> length (map f as) === length as
 210 | mapLen f []        = Refl
 211 | mapLen f (x :: xs) = cong S $ mapLen f xs
 212 | 
 213 | ||| Create a `Graph` from a list of labeled nodes and edges.
 214 | export
 215 | mkGraphL : (ns : List n) -> List (Edge (length ns) e) -> IGraph (length ns) e n
 216 | mkGraphL ns es =
 217 |   IG $ allocListWith ns (`A` empty) $ \r,t =>
 218 |     let _ # t := linsEdges r es t
 219 |      in unsafeFreeze r t
 220 | 
 221 | ||| Create a `Graph` from a vect of labeled nodes and edges.
 222 | export
 223 | mkGraph : {k : _} -> (ns : Vect k n) -> List (Edge k e) -> IGraph k e n
 224 | mkGraph ns es =
 225 |   IG $ allocVect (map (`A` empty) ns) $ \r,t =>
 226 |     let _ # t := linsEdges r es t
 227 |      in unsafeFreeze r t
 228 | 
 229 | ||| Create a `Graph` from a vect of labeled nodes and edges.
 230 | |||
 231 | ||| Unlike `mkGraph`, this puts the nodes in the array in reverse order,
 232 | ||| which is useful when they come from a parser with the last node being
 233 | ||| at the head of the vector.
 234 | export
 235 | mkGraphRev : {k : _} -> (ns : Vect k n) -> List (Edge k e) -> IGraph k e n
 236 | mkGraphRev ns es =
 237 |  IG $ allocVectRev (map (`A` empty) ns) $ \r,t =>
 238 |    let _ # t := linsEdges r es t
 239 |     in unsafeFreeze r t
 240 | 
 241 | export %inline
 242 | generate : (k : Nat) -> (Fin k -> Adj k e n) -> IGraph k e n
 243 | generate k f = IG $ generate k f
 244 | 
 245 | --------------------------------------------------------------------------------
 246 | --          Folds and Traversals
 247 | --------------------------------------------------------------------------------
 248 | 
 249 | ||| Map the adjacencies in a graph accoring to each node's context
 250 | export %inline
 251 | mapCtxt :
 252 |      {k : _}
 253 |   -> (Fin k -> Adj k e n -> Adj k e1 n1)
 254 |   -> IGraph k e n
 255 |   -> IGraph k e1 n1
 256 | mapCtxt fun (IG g) = IG $ mapWithIndex fun g
 257 | 
 258 | ||| Map the node labels in a graph accoring to each node's context
 259 | export %inline
 260 | mapWithCtxt :
 261 |      {k : _}
 262 |   -> (Fin k -> Adj k e n -> n1)
 263 |   -> IGraph k e n
 264 |   -> IGraph k e n1
 265 | mapWithCtxt fun = mapCtxt (\x,adj => adj $> fun x adj)
 266 | 
 267 | ||| Map the adjacencies in a graph
 268 | export %inline
 269 | mapAdj : {k : _} -> (Adj k e n -> Adj k f m) -> IGraph k e n -> IGraph k f m
 270 | mapAdj fun (IG g) = IG $ map fun g
 271 | 
 272 | ||| Map the node labels in a graph accoring to each node's adjacency
 273 | export %inline
 274 | mapWithAdj : {k : _} -> (Adj k e n -> m) -> IGraph k e n -> IGraph k e m
 275 | mapWithAdj fun = mapAdj (\adj => adj $> fun adj)
 276 | 
 277 | export
 278 | traverseCtxt :
 279 |      {k : _}
 280 |   -> {auto app : Applicative f}
 281 |   -> (Fin k -> Adj k e n -> f (Adj k e1 n1))
 282 |   -> IGraph k e n
 283 |   -> f (IGraph k e1 n1)
 284 | traverseCtxt fun (IG g) = IG <$> traverseWithIndex fun g
 285 | 
 286 | export
 287 | traverseWithCtxt :
 288 |      {k : _}
 289 |   -> {auto app : Applicative f}
 290 |   -> (Fin k -> Adj k e n -> f n1)
 291 |   -> IGraph k e n
 292 |   -> f (IGraph k e n1)
 293 | traverseWithCtxt fun = traverseCtxt (\x,a => (`A` a.neighbours) <$> fun x a)
 294 | 
 295 | --------------------------------------------------------------------------------
 296 | --          Modifying Graphs
 297 | --------------------------------------------------------------------------------
 298 | 
 299 | ||| Uses two functions for updating nodes in a graph:
 300 | |||
 301 | ||| Once is used for the given node, the other for all other nodes.
 302 | export
 303 | updateNodes : {k : _} -> Fin k -> (f,g : m -> n) -> IGraph k e m -> IGraph k e n
 304 | updateNodes x f g = mapWithCtxt (\y,a => if x == y then f a.label else g a.label)
 305 | 
 306 | ||| Updates a single node in the graph at the given position.
 307 | export %inline
 308 | updateNode : {k : _} -> Fin k -> (n -> n) -> IGraph k e n -> IGraph k e n
 309 | updateNode x f = updateNodes x f id
 310 | 
 311 | ||| Replaces a single node in the graph at the given position.
 312 | export %inline
 313 | setNode : {k : _} -> Fin k -> n -> IGraph k e n -> IGraph k e n
 314 | setNode x = updateNode x . const
 315 | 
 316 | ||| Uses two functions for updating the edge labels in a graph.
 317 | |||
 318 | ||| Once is used for the edge connecting the two given nodes, the other for
 319 | ||| all other edges.
 320 | export
 321 | updateEdges :
 322 |      {k : _}
 323 |   -> (x,y : Fin k)
 324 |   -> (f,g : e -> e2)
 325 |   -> IGraph k e n
 326 |   -> IGraph k e2 n
 327 | updateEdges x y f g =
 328 |   mapCtxt $ \k,(A l a) =>
 329 |    A l $
 330 |      if      k == x then mapKV (\m,l => if m == y then f l else g l) a
 331 |      else if k == y then mapKV (\m,l => if m == x then f l else g l) a
 332 |      else    map g a
 333 | 
 334 | ||| Uses a function for updating a single edge label in a graph.
 335 | export %inline
 336 | updateEdge :
 337 |      {k : _}
 338 |   -> (x,y : Fin k)
 339 |   -> (f : e -> e)
 340 |   -> IGraph k e n
 341 |   -> IGraph k e n
 342 | updateEdge x y f = updateEdges x y f id
 343 | 
 344 | ||| Insert (or replace) a single edge in a graph.
 345 | export
 346 | insEdges : {k : _} -> List (Edge k e) -> IGraph k e n -> IGraph k e n
 347 | insEdges es g =
 348 |   IG $ allocGen k (adj g) $ \r,t =>
 349 |     let _ # t := linsEdges r es t
 350 |      in unsafeFreeze r t
 351 | 
 352 | ||| Insert an `Edge` into the 'IGraph'.
 353 | export %inline
 354 | insEdge : {k : _} -> Edge k e -> IGraph k e n -> IGraph k e n
 355 | insEdge = insEdges . pure
 356 | 
 357 | ||| Remove multiple 'Edge's from the 'Graph'.
 358 | export
 359 | delEdges : {k : _} -> List (Fin k, Fin k) -> IGraph k e n -> IGraph k e n
 360 | delEdges ps g = IG $ allocGen k (adj g) $ \r,t =>
 361 |   let _ # t := ldelEdges r ps t
 362 |    in unsafeFreeze r t
 363 | 
 364 | ||| Remove an 'Edge' from the 'Graph'.
 365 | export %inline
 366 | delEdge : {k : _} -> (x,y : Fin k) -> IGraph k e n -> IGraph k e n
 367 | delEdge x y = delEdges [(x,y)]
 368 | 
 369 | ||| Insert multiple `LNode`s into the `Graph`.
 370 | export
 371 | insNodes : {k,m : _} -> IGraph k e n -> (ns : Vect m n) -> IGraph (k + m) e n
 372 | insNodes (IG g) ns =
 373 |   let g'  := map (weakenAdjN m) g
 374 |    in IG $ append g' (map fromLabel (array ns))
 375 | 
 376 | ||| Insert multiple `LNode`s into the `Graph`.
 377 | export
 378 | insNodesAndEdges :
 379 |      {k,m : _}
 380 |   -> IGraph k e n
 381 |   -> (ns : Vect m n)
 382 |   -> (es : List (Edge (k + m) e))
 383 |   -> IGraph (k + m) e n
 384 | insNodesAndEdges g ns es = insEdges es $ insNodes g ns
 385 | 
 386 | ||| Insert a labeled node into the `Graph`.
 387 | ||| The behavior is undefined if the node is already
 388 | ||| in the graph.
 389 | export %inline
 390 | insNode : {k : _} -> IGraph k e n -> n -> IGraph (S k) e n
 391 | insNode g v = rewrite plusCommutative 1 k in insNodes g [v]
 392 | 
 393 | export
 394 | adjEdges : SortedMap (Fin x) (Fin y) -> Adj x e n -> Adj y e n
 395 | adjEdges m (A l ns) =
 396 |   let ps := mapMaybe (\(n,v) => (,v) <$> lookup n m) $ pairs ns
 397 |    in A l $ fromList ps
 398 | 
 399 | zipTR : SnocList (a,b) -> List a -> List b -> List (a,b)
 400 | zipTR sx []        _         = sx <>> []
 401 | zipTR sx _         []        = sx <>> []
 402 | zipTR sx (x :: xs) (y :: ys) = zipTR (sx:<(x,y)) xs ys
 403 | 
 404 | export
 405 | delNodes : {k : _} -> List (Fin k) -> IGraph k e n -> Graph e n
 406 | delNodes {k = 0} _ _ = G _ empty
 407 | delNodes {k = S x} ks (IG g) =
 408 |   let set       := SortedSet.fromList ks
 409 |       A (S y) h :=
 410 |         filterWithKey (\x,_ => not (contains x set)) g | A 0 _ => G _ empty
 411 |       finX      := filter (\x => not (contains x set)) $ allFinsFast (S x)
 412 |       finY      := allFinsFast (S y)
 413 |       proMap    := SortedMap.fromList $ zipTR [<] finX finY
 414 |    in G (S y) (IG $ map (adjEdges proMap) h)
 415 | 
 416 | ||| Remove a 'Node' from the 'Graph'.
 417 | export
 418 | delNode : {k : _} -> Fin k -> IGraph k e n -> Graph e n
 419 | delNode = delNodes . pure
 420 | 
 421 | ||| Merge two graphs connecting them via the given list of
 422 | ||| edges
 423 | export
 424 | mergeGraphsWithEdges :
 425 |      {k,m : _}
 426 |   -> (g1 : IGraph k e n)
 427 |   -> (g2 : IGraph m e n)
 428 |   -> List (Fin k, Fin m, e)
 429 |   -> IGraph (k + m) e n
 430 | mergeGraphsWithEdges {k} g t es =
 431 |   let vNodes := label <$> toVect t.graph
 432 |       cEdges := map (\(x,y,l) => compositeEdge x y l) es
 433 |       lEdges := incEdge k <$> edges t
 434 |    in insNodesAndEdges g vNodes (cEdges ++ lEdges)
 435 | 
 436 | ||| Merge two graphs that have no bonds between them.
 437 | export
 438 | mergeGraphs :
 439 |      {k,m : _}
 440 |   -> (g1 : IGraph k e n)
 441 |   -> (g2 : IGraph m e n)
 442 |   -> IGraph (k + m) e n
 443 | mergeGraphs {k} g t =
 444 |   let vNodes := label <$> toVect t.graph
 445 |       lEdges := incEdge k <$> edges t
 446 |    in insNodesAndEdges g vNodes lEdges
 447 | 
 448 | --------------------------------------------------------------------------------
 449 | --          Displaying Graphs
 450 | --------------------------------------------------------------------------------
 451 | 
 452 | export
 453 | {k : _} -> Show e => Show n => Show (IGraph k e n) where
 454 |   showPrec p g = showCon p "mkGraph" $ showArg (labels g) ++ showArg (edges g)
 455 | 
 456 | export
 457 | Show e => Show n => Show (Graph e n) where
 458 |   showPrec p (G o g) = showCon p "G" $ showArg o ++ showArg g
 459 | 
 460 | pl : Nat -> Fin k -> String
 461 | pl n = padLeft n ' ' . show . finToNat
 462 | 
 463 | export
 464 | pretty : {k : _} -> (e -> String) -> (n -> String) -> IGraph k e n -> String
 465 | pretty de dn g =
 466 |   let ns     := labNodes g
 467 |       es     := edges g
 468 |       maxLen := length $ show k
 469 |    in unlines $
 470 |         "Nodes:"   :: map (dispNode maxLen) ns ++
 471 |         "\nEdges:" :: map (dispEdge maxLen) es
 472 | 
 473 |   where
 474 |     dispNode : Nat -> (Fin k, n) -> String
 475 |     dispNode k (n1,l) =
 476 |       "  \{pl k n1} :> \{dn l}"
 477 | 
 478 |     dispEdge : Nat -> Edge k e -> String
 479 |     dispEdge k (E n1 n2 l) =
 480 |       "E \{pl k n1} \{pl k n2}  \{de l}"
 481 |