0 | module Data.Graph.Indexed.Query.BFS
  1 |
  2 | import Data.Queue
  3 | import Data.Graph.Indexed
  4 | import Data.Graph.Indexed.Query.Util
  5 | import Data.Graph.Indexed.Query.Visited
  6 | import Data.SnocList
  7 |
  8 | %default total
  9 |
 10 | enqueueE :
 11 |      Queue (s, Fin k)
 12 |   -> (s -> Fin k -> Either s a)
 13 |   -> s
 14 |   -> List (Fin k)
 15 |   -> Either (Queue (s, Fin k)) a
 16 | enqueueE q f st []      = Left q
 17 | enqueueE q f st (x::xs) =
 18 |   case f st x of
 19 |     Right v => Right v
 20 |     Left st2 => enqueueE (enqueue q (st2, x)) f st xs
 21 |
 22 | parameters {k : Nat}
 23 |            (g : IGraph k e n)
 24 |
 25 | --------------------------------------------------------------------------------
 26 | -- Flat BFS traversals
 27 | --------------------------------------------------------------------------------
 28 |
 29 |   -- flat BFS implementation for large graphs
 30 |   bfsL : Queue (s,Fin k) -> (s -> Fin k -> Either s a) -> MVis t k (Maybe a)
 31 |   bfsL q f r t =
 32 |     case dequeue q of
 33 |       Nothing => Nothing # t
 34 |       Just ((vs,x),q2) =>
 35 |        let False # t := mvisited r x t
 36 |              | True # t => bfsL q2 f (assert_smaller r r) t
 37 |            Left q3 := enqueueE q2 f vs (neighbours g x) | Right v => Just v # t
 38 |            _ # t := mvisit r x t
 39 |         in bfsL q3 f (assert_smaller r r) t
 40 |
 41 |   ||| Traverses the graph in breadth-first order for the given
 42 |   ||| start nodes and accumulates the nodes encountered with the
 43 |   ||| given function.
 44 |   |||
 45 |   ||| Unlike `bfsWith`, this takes a list of nodes that are taboo, that is
 46 |   ||| that will already be set to `visited`. This allows us exclude certain
 47 |   ||| pathways from our search.
 48 |   |||
 49 |   ||| One use case is to find the shortest cycle containing a given
 50 |   ||| edge or sequence of edges.
 51 |   export
 52 |   limitedBfsWith :
 53 |        (taboo : List (Fin k))
 54 |     -> (s -> Fin k -> Either s a)
 55 |     -> (init : s)
 56 |     -> Fin k
 57 |     -> Maybe a
 58 |   limitedBfsWith taboo acc init x =
 59 |     visiting k $ \r,t =>
 60 |       let _ # t := mvisitAll r taboo t
 61 |        in bfsL (fromList [(init,x)]) acc r t
 62 |
 63 |   ||| Traverses the graph in breadth-first order for the given
 64 |   ||| start nodes and accumulates the nodes encountered with the
 65 |   ||| given function.
 66 |   export %inline
 67 |   bfsWith : (s -> Fin k -> Either s a) -> (init : s) -> Fin k -> Maybe a
 68 |   bfsWith = limitedBfsWith []
 69 |
 70 |   ||| Tries to find a shortest path between the two nodes.
 71 |   export %inline
 72 |   limitedBfs :
 73 |        (taboo : List (Fin k))
 74 |      -> Fin k
 75 |      -> Fin k
 76 |      -> Maybe (SnocList (Fin k))
 77 |   limitedBfs taboo start end =
 78 |     if start == end then Just [< start]
 79 |     else
 80 |       limitedBfsWith
 81 |         taboo
 82 |         (\sx,x => if x == end then Right (sx :< x) else Left (sx :< x))
 83 |         [<start]
 84 |         start
 85 |
 86 |   ||| Tries to find a shortest path between the two nodes.
 87 |   export %inline
 88 |   bfs : Fin k -> Fin k -> Maybe (SnocList (Fin k))
 89 |   bfs = limitedBfs []
 90 |
 91 | ----------------------------------------------------------------------------------
 92 | ---- Generalized Breadth-First Searches
 93 | ----------------------------------------------------------------------------------
 94 |
 95 |   -- BFS implementation covering a whole connected component for large graphs
 96 |   bfsAllL : SnocList s -> Queue (s,Fin k) -> (s -> Fin k -> s) -> MVis t k (List s)
 97 |   bfsAllL ss q f r t =
 98 |     case dequeue q of
 99 |       Nothing => (ss <>> []) # t
100 |       Just ((vs,x),q2) =>
101 |        let False # t := mvisited r x t
102 |              | True # t => bfsAllL ss q2 f (assert_smaller r r) t
103 |            q3 := enqueueAll q2 (map (\y => (f vs y, y)) $ neighbours g x)
104 |            _ # t := mvisit r x t
105 |         in bfsAllL (ss :< vs) q3 f (assert_smaller r r) t
106 |
107 |   ||| Traverses the graph in breadth-first order for the given
108 |   ||| start nodes and accumulates the nodes encountered with the
109 |   ||| given function.
110 |   export
111 |   bfsAllWith : (s -> Fin k -> s) -> (init : s) -> Fin k -> List s
112 |   bfsAllWith acc init x =
113 |     visiting k (bfsAllL [<] (fromList [(init,x)]) acc)
114 |
115 |   export
116 |   distancesToNode : Fin k -> List (Nat, Fin k)
117 |   distancesToNode x = bfsAllWith (\x,y => (S $ fst x, y)) (0,x) x
118 |
119 | ----------------------------------------------------------------------------------
120 | ---- Shortest Paths
121 | ----------------------------------------------------------------------------------
122 |
123 |   covering
124 |   shortestL :
125 |        SnocList (SnocList $ Fin k)
126 |     -> Queue (SnocList $ Fin k)
127 |     -> MVis t k (List (SnocList $ Fin k))
128 |   shortestL sp q r t =
129 |     case dequeue q of
130 |       Nothing => (sp <>> []) # t
131 |       Just (sx@(_:<x),q2) =>
132 |         let False # t := mvisited r x t | True # t => shortestL sp q2 r t
133 |             ns := map (sx :<) (neighbours g x)
134 |             _ # t := mvisit r x t
135 |          in shortestL (sp :< sx) (enqueueAll q2 ns) r t
136 |       Just (_,q2) => shortestL sp q2 r t
137 |
138 |   ||| Computes the shortest paths to all nodes reachable from
139 |   ||| the given starting node. This is a simplified version of
140 |   ||| Dijkstra's algorithm for unweighted edges.
141 |   |||
142 |   ||| Runs in O(n+m) time and O(n) memory.
143 |   export
144 |   shortestPaths : Fin k -> List (SnocList $ Fin k)
145 |   shortestPaths x =
146 |     let q := fromList $ map ([<x] :<) (neighbours g x)
147 |      in assert_total $
148 |           visiting k $ \r,t => let _ # t := mvisit r x t in shortestL [<] q r t
149 |