0 | module Libraries.Data.Graph
 1 |
 2 | import Data.List1
 3 | import Data.SortedMap
 4 | import Data.SortedSet
 5 |
 6 | -- Mechanically transcribed from
 7 | -- https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm#The_algorithm_in_pseudocode
 8 | private
 9 | record TarjanVertex where
10 |   constructor TV
11 |   index   : Int
12 |   lowlink : Int
13 |   inStack : Bool
14 |
15 | private
16 | record TarjanState cuid where
17 |   constructor TS
18 |   vertices           : SortedMap cuid TarjanVertex
19 |   stack              : List cuid
20 |   nextIndex          : Int
21 |   components         : List (List1 cuid)
22 |   impossibleHappened : Bool  -- we should get at least some indication of broken assumptions
23 |
24 | initial : Ord cuid => TarjanState cuid
25 | initial = TS empty [] 0 [] False
26 |
27 | ||| Find strongly connected components in the given graph.
28 | |||
29 | ||| Input: map from vertex X to all vertices Y such that there is edge X->Y
30 | ||| Output: list of strongly connected components, ordered by output degree descending
31 | export
32 | tarjan : Ord cuid => SortedMap cuid (SortedSet cuid) -> List (List1 cuid)
33 | tarjan {cuid} deps = loop initial (SortedMap.keys deps)
34 |   where
35 |     strongConnect : TarjanState cuid -> cuid -> TarjanState cuid
36 |     strongConnect ts v =
37 |         let ts'' = case SortedMap.lookup v deps of
38 |               Nothing => ts'  -- no edges
39 |               Just edgeSet => loop ts' (Prelude.toList edgeSet)
40 |           in case SortedMap.lookup v ts''.vertices of
41 |               Nothing => { impossibleHappened := True } ts''
42 |               Just vtv =>
43 |                 if vtv.index == vtv.lowlink
44 |                   then createComponent ts'' v []
45 |                   else ts''
46 |       where
47 |         createComponent : TarjanState cuid -> cuid -> List cuid -> TarjanState cuid
48 |         createComponent ts v acc =
49 |           case ts.stack of
50 |             [] => { impossibleHappened := True } ts
51 |             w :: ws =>
52 |               let ts' : TarjanState cuid = {
53 |                       vertices $= updateExisting { inStack := False } w,
54 |                       stack := ws
55 |                     } ts
56 |                 in if w == v
57 |                   then { components $= ((v ::: acc) ::) } ts'  -- that's it
58 |                   else createComponent ts' v (w :: acc)
59 |
60 |         loop : TarjanState cuid -> List cuid -> TarjanState cuid
61 |         loop ts [] = ts
62 |         loop ts (w :: ws) =
63 |           loop (
64 |             case SortedMap.lookup w ts.vertices of
65 |               Nothing => let ts' = strongConnect ts w in
66 |                 case SortedMap.lookup w ts'.vertices of
67 |                   Nothing => { impossibleHappened := True } ts'
68 |                   Just wtv => { vertices $= updateExisting { lowlink $= min wtv.lowlink } v } ts'
69 |
70 |               Just wtv => case wtv.inStack of
71 |                 False => ts  -- nothing to do
72 |                 True => { vertices $= updateExisting { lowlink $= min wtv.index } v } ts
73 |           ) ws
74 |
75 |         ts' : TarjanState cuid
76 |         ts' = {
77 |             vertices  $= SortedMap.insert v (TV ts.nextIndex ts.nextIndex True),
78 |             stack     $= (v ::),
79 |             nextIndex $= (1+)
80 |           } ts
81 |
82 |     loop : TarjanState cuid -> List cuid -> List (List1 cuid)
83 |     loop ts [] =
84 |       if ts.impossibleHappened
85 |         then []
86 |         else ts.components
87 |     loop ts (v :: vs) =
88 |       case SortedMap.lookup v ts.vertices of
89 |         Just _ => loop ts vs  -- done, skip
90 |         Nothing => loop (strongConnect ts v) vs
91 |