Data.Graph.Indexed.Query.Visited

Reexports

Definitions

mvisit : MBuffer s n -> Fin n -> F1' s

  Set the current node to "visited".

Totality: total
Visibility: export

mvisitAll : MBuffer s n -> List (Fin n) -> F1' s

  Set all given nodes to "visited"

Totality: total
Visibility: export

mvisited : MBuffer s n -> Fin n -> F1 s Bool

  True, if the current node has been visited.

Totality: total
Visibility: export

munvisited : MBuffer s n -> Fin n -> F1 s Bool

  True, if the current node has not yet been visited.

Totality: total
Visibility: export

visiting : (k : Nat) -> WithMBuffer k a -> a

  Allocate a linear byte array and use it to run the given
  computation, discarding it at the end.
  
  This is a convenience alias for `visiting` for those cases, where
  we already have a function returning a linear pair of values.

Totality: total
Visibility: export

record Visited : Nat -> Type

  Immutable value for keeping track of the visited nodes in a graph.
  
  Note: Profiling on the Chez backend showed, that this is considerably
        faster than `MVisited` for `k < 64`. For larger `k`, however,
        `MVisited` outperforms this by far.

Totality: total
Visibility: export
Constructor: 

V : Integer -> Visited k

Projection: 

.vis : Visited k -> Integer

ini : Visited k

  Initial `Visited` state

Totality: total
Visibility: export

visit : Fin k -> Visited k -> Visited k

  Set the current node to "visited".

Totality: total
Visibility: export

visitAll : List (Fin k) -> Visited k -> Visited k

  Set all given nodes to "visited".

Totality: total
Visibility: export

visited : Fin k -> Visited k -> Bool

  True, if the current node has been visited.

Totality: total
Visibility: export

unvisited : Fin k -> Visited k -> Bool

  True, if the current node has not yet been visited.

Totality: total
Visibility: export