3 | module Data.Graph.Indexed.Query.DFS
7 | import Data.Graph.Indexed
8 | import Data.Graph.Indexed.Query.Util
9 | import Data.Graph.Indexed.Query.Visited
13 | parameters {k : Nat}
21 | dfsL : List (Fin k) -> (s -> Fin k -> Either s a) -> s -> MVis t k (Either s a)
22 | dfsL [] f st r t = Left st # t
23 | dfsL (x::xs) f st r t =
24 | let False # t := mvisited r x t | True # t => dfsL xs f st (assert_smaller r r) t
25 | Left st2 := f st x | Right v => Right v # t
26 | _ # t := mvisit r x t
27 | in dfsL (neighbours g x ++ xs) f st2 (assert_smaller r r) t
29 | %inline dfsL' : List (Fin k) -> (s -> Fin k -> s) -> s -> MVis t k s
30 | dfsL' xs acc i r t = fromLeftMVis $
dfsL xs (fleft2 acc) i r t
45 | (taboo : List (Fin k))
46 | -> (s -> Fin k -> Either s a)
50 | limitedDfsWith taboo acc init x =
51 | visiting k $
\r,t =>
52 | let _ # t := mvisitAll r taboo t
53 | in dfsL [x] acc init r t
63 | dfsWith : (s -> Fin k -> Either s a) -> (init : s) -> Fin k -> Either s a
64 | dfsWith = limitedDfsWith []
70 | (taboo : List (Fin k))
71 | -> (acc : s -> Fin k -> s)
75 | limitedDfsWith' taboo acc init =
76 | fromLeft . limitedDfsWith taboo (fleft2 acc) init
81 | dfsWith' : (acc : s -> Fin k -> s) -> (init : s) -> Fin k -> s
82 | dfsWith' = limitedDfsWith' []
87 | limitedDfs : (taboo : List (Fin k)) -> Fin k -> SnocList (Fin k)
88 | limitedDfs taboo = limitedDfsWith' taboo (:<) [<]
93 | dfs : Fin k -> SnocList (Fin k)
101 | cdfsL : (s -> Fin k -> s) -> s -> SnocList s -> List (Fin k) -> MVis t k (List s)
102 | cdfsL f i ss [] r t = (ss <>> []) # t
103 | cdfsL f i ss (x::xs) r t =
104 | let False # t := mvisited r x t | True # t => cdfsL f i ss xs r t
105 | y # t := dfsL' [x] f i r t
106 | in cdfsL f i (ss:<y) xs r t
115 | cdfsWith : (acc : s -> Fin k -> s) -> (init : s) -> List (Fin k) -> List s
116 | cdfsWith acc init xs = visiting k (cdfsL acc init [<] xs)
121 | cdfsWith' : (acc : s -> Fin k -> s) -> (init : s) -> List s
122 | cdfsWith' acc init = cdfsWith acc init (allFinsFast k)
127 | cdfs : List (Fin k) -> List (SnocList (Fin k))
128 | cdfs = cdfsWith (:<) [<]
133 | cdfs' : List (SnocList (Fin k))
134 | cdfs' = cdfsWith' (:<) [<]
141 | dffL : (Fin k -> s) -> List (Fin k) -> MVis t k (Forest s)
142 | dffL f [] r t = [] # t
143 | dffL f (x::xs) r t =
144 | let False # t := mvisited r x t
145 | | True # t => dffL f xs (assert_smaller r r) t
146 | _ # t := mvisit r x t
147 | ts # t := dffL f (neighbours g x) (assert_smaller r r) t
148 | fs # t := dffL f xs (assert_smaller r r) t
149 | in (T (f x) ts :: fs) # t
158 | dffWith : (Fin k -> t) -> List (Fin k) -> Forest t
159 | dffWith f xs = visiting k (dffL f xs)
167 | dffWith' : (Fin k -> t) -> Forest t
168 | dffWith' f = dffWith f (allFinsFast k)
176 | dff : List (Fin k) -> Forest (Fin k)
185 | dff' : Forest (Fin k)
194 | components : List (SnocList $
Fin k)
200 | noComponents = length components
205 | isConnected = noComponents == 1