0 | module Data.Graph.Indexed.Query.Visited
 1 |
 2 | import Data.Bits
 3 | import Data.Buffer
 4 | import Data.Linear.Traverse1
 5 | import public Data.Buffer.Mutable
 6 |
 7 | %default total
 8 |
 9 | --------------------------------------------------------------------------------
10 | --          MVisited
11 | --------------------------------------------------------------------------------
12 |
13 | parameters (r : MBuffer s n)
14 |
15 |   ||| Set the current node to "visited".
16 |   export %inline
17 |   mvisit : Fin n -> F1' s
18 |   mvisit i = set r i 1
19 |
20 |   ||| Set all given nodes to "visited"
21 |   export %inline
22 |   mvisitAll : List (Fin n) -> F1' s
23 |   mvisitAll = traverse1_ mvisit
24 |
25 |   ||| True, if the current node has been visited.
26 |   export %inline
27 |   mvisited : Fin n -> F1 s Bool
28 |   mvisited x t =
29 |     case get r x t of
30 |       1 # t => True  # t
31 |       _ # t => False # t
32 |
33 |   ||| True, if the current node has not yet been visited.
34 |   export %inline
35 |   munvisited : Fin n -> F1 s Bool
36 |   munvisited x t =
37 |     case get r x t of
38 |       1 # t => False # t
39 |       _ # t => True  # t
40 |
41 | ||| Allocate a linear byte array and use it to run the given
42 | ||| computation, discarding it at the end.
43 | |||
44 | ||| This is a convenience alias for `visiting` for those cases, where
45 | ||| we already have a function returning a linear pair of values.
46 | export %inline
47 | visiting : (k : Nat) -> WithMBuffer k a -> a
48 | visiting = alloc
49 |
50 | --------------------------------------------------------------------------------
51 | --          Visited
52 | --------------------------------------------------------------------------------
53 |
54 | ||| Immutable value for keeping track of the visited nodes in a graph.
55 | |||
56 | ||| Note: Profiling on the Chez backend showed, that this is considerably
57 | |||       faster than `MVisited` for `k < 64`. For larger `k`, however,
58 | |||       `MVisited` outperforms this by far.
59 | export
60 | record Visited (k : Nat) where
61 |   constructor V
62 |   vis : Integer
63 |
64 | ||| Initial `Visited` state
65 | export
66 | ini : Visited k
67 | ini = V 0
68 |
69 | ||| Set the current node to "visited".
70 | export
71 | visit : Fin k -> Visited k -> Visited k
72 | visit i (V b) = V $ setBit b (finToNat i)
73 |
74 | ||| Set all given nodes to "visited".
75 | export %inline
76 | visitAll : List (Fin k) -> Visited k -> Visited k
77 | visitAll vs v = foldl (flip visit) v vs
78 |
79 | ||| True, if the current node has been visited.
80 | export %inline
81 | visited : Fin k -> Visited k -> Bool
82 | visited i (V b) = testBit b (finToNat i)
83 |
84 | ||| True, if the current node has not yet been visited.
85 | export %inline
86 | unvisited : Fin k -> Visited k -> Bool
87 | unvisited i = not . visited i
88 |