0 | ||| This module provides utilities used to compute families of relevant cycles
  1 | ||| as described by Vismara et al in "Union of all the minimum cycle bases of a graph"
  2 | ||| (The Electronic Journal of Combinatorics 4 (1997)).
  3 | |||
  4 | ||| In particular, it computes the number of shortest paths between a root
  5 | ||| node and all other nodes in a graph.
  6 | |||
  7 | ||| Please note that this is internal stuff. The algorithm is not suitable
  8 | ||| as a general shortest path algorithm, as it computes only paths up
  9 | ||| to half the graph order in length.
 10 | module Data.Graph.Indexed.Ring.Relevant.ShortestPath
 11 |
 12 | import Data.Array.Mutable
 13 | import Data.Graph.Indexed.Ring.Relevant.Types
 14 | import Data.Linear.Ref1
 15 | import Data.List
 16 | import Data.Queue
 17 | import public Data.Graph.Indexed
 18 | import public Data.Graph.Indexed.Subgraph
 19 |
 20 | %default total
 21 |
 22 | ||| `True` if node `n` is "smaller" than `root`. This is
 23 | ||| the ordering "pi" used in the paper.
 24 | export %inline
 25 | smaller : Fin o -> (rdeg : Nat) -> ISubgraph o k e Nat -> Fin o -> Bool
 26 | smaller root rdeg g n =
 27 |   case compare (snd $ lab g n) rdeg of
 28 |     LT => True
 29 |     EQ => root < n
 30 |     GT => False
 31 |
 32 | parameters {o    : Nat}
 33 |            (g    : ISubgraph o k e Nat)
 34 |            (root : Fin o)
 35 |            (rdeg : Nat)
 36 |            (q    : Ref s (Queue $ Fin o))
 37 |            (r    : MArray s o (Path o))
 38 |
 39 |   -- dequeue a value from the mutable queue
 40 |   %inline
 41 |   deq : F1 s (Maybe $ Fin o)
 42 |   deq t =
 43 |    let qu # t := read1 q t
 44 |     in case dequeue qu of
 45 |          Nothing     => Nothing # t
 46 |          Just (v,q2) => let _ # t := write1 q q2 t in Just v # t
 47 |
 48 |   -- enqueue a value at the mutable queue
 49 |   %inline
 50 |   enq : Fin o -> F1' s
 51 |   enq v t = let qu # t := read1 q t in write1 q (enqueue qu v) t
 52 |
 53 |   -- Appends a node to a path. This also updates the `length` and `last` node.
 54 |   append : Path o -> Fin o -> Path o
 55 |   append (P l p k fs ls c) n =
 56 |     -- initially, a `Path` has set its `first` node to `root`.
 57 |     -- If that's the case, we are at first node after root.
 58 |     -- Note: Paths are only to be kept, if all their nodes are
 59 |     -- `smaller` than the root node.
 60 |     if fs == root
 61 |        then P (S l) (p :< n) (smaller root rdeg g n)      n  n c
 62 |        else P (S l) (p :< n) (k && smaller root rdeg g n) fs n c
 63 |
 64 |   -- two paths from `root` to `n` are to be combined, if
 65 |   -- they are of the same length and both are to be kept.
 66 |   -- `n` will be appended to `p`. `q` already has `n` as its
 67 |   -- last node.
 68 |   merge : Path o -> Fin o -> Path o -> Path o
 69 |   merge p n q =
 70 |     let True := S p.length == q.length | False => q
 71 |         True := p.keep                 | False => q
 72 |         True := q.keep                 | False => append p n
 73 |      in {combos $= (+ p.combos)} q
 74 |
 75 |   -- process the neighbours of the last node of the given path
 76 |   adjNeighbours : Path o -> List (Fin o) -> F1' s
 77 |   adjNeighbours p []      t = () # t
 78 |   adjNeighbours p (x::xs) t =
 79 |     let p2 # t := Core.get r x t
 80 |      in case p2.length of
 81 |           -- `x` has not yet ben processed. append it to `p` and enqeueue it.
 82 |           Z =>
 83 |            let _ # t  := set r x (append p x) t
 84 |                _ # t  := enq x t
 85 |             in adjNeighbours p xs t
 86 |           -- `x` has been processed. merge the two paths but don't enqueue it
 87 |           _ =>
 88 |            let _ # t := set r x (merge p x p2) t
 89 |             in adjNeighbours p xs t
 90 |
 91 |   covering
 92 |   impl : SnocList (Path o) -> F1 s (List $ Path o)
 93 |   impl sp t =
 94 |     -- process the next enqueued node and the path associated with it
 95 |     case deq t of
 96 |       Nothing # t => (sp <>> []) # t
 97 |       Just n  # t =>
 98 |        let p # t := Core.get r n t
 99 |            False := p.length * 2 > o | True => (sp <>> []) # t -- abort early
100 |            _ # t := adjNeighbours p (neighbours g n) t
101 |         in impl (if p.keep then sp :< p else sp) t
102 |
103 | ||| Converts a subgraph to hold the degree of each node as its label.
104 | export
105 | toDegs : Subgraph k e n -> Subgraph k e Nat
106 | toDegs (G o g) = G o $ mapAdj (\(A (x,_) ns) => A (x, length ns) ns) g
107 |
108 | ||| Computes the shortest paths to all nodes reachable from
109 | ||| the given starting node.
110 | |||
111 | ||| Note: This is not a general shortest paths algorithm but a utility
112 | ||| for computing relevant cycles. Since paths are later merged to cycles,
113 | ||| only paths of length up to half the graph order are computed.
114 | export
115 | shortestPaths : {o : _} -> ISubgraph o k e Nat -> Fin o -> List (Path o)
116 | shortestPaths g root =
117 |   assert_total $ run1 $ \t =>
118 |     let r # t := marray1 o (P 0 [<] False root root 0) t
119 |         q # t := ref1 (Queue.fromList [root]) t
120 |         _ # t := set r root (P 1 [<root] False root root 1) t
121 |      in impl g root (snd $ lab g root) q r [<] t
122 |