# Depth first search #

We perform depth first search of a tree or graph, where the neighbours of a vertex are provided either by list α → List α or a lazy list α → MLList MetaM α.

This is useful in meta code for searching for solutions in the presence of alternatives. It can be nice to represent the choices via a lazy list, so the later choices don't need to be evaluated while we do depth first search on earlier choices.

partial def depthFirst' {m : Type u_1 → Type u_1} [] [] {α : Type u_1} (f : Natαm α) (n : Nat) (a : α) :
m α

A generalisation of depthFirst, which allows the generation function to know the current depth, and to count the depth starting from a specified value.

def depthFirst {m : Type u_1 → Type u_1} [] [] {α : Type u_1} (f : αm α) (a : α) (maxDepth : optParam () none) :
m α

Depth first search of a graph generated by a function f : α → m α.

Here m must be an Alternative Monad, and perhaps the only sensible values are List and MLList MetaM.

The option maxDepth limits the search depth.

Note that if the graph is not a tree then elements will be visited multiple times. (See depthFirstRemovingDuplicates)

Equations
Instances For
def depthFirstRemovingDuplicates {m : Type u → Type u} [] {α : Type u} [BEq α] [] (f : αMLList m α) (a : α) (maxDepth : optParam () none) :
MLList m α

Variant of depthFirst, using an internal HashSet to record and avoid already visited nodes.

This version describes the graph using α → MLList m α, and returns the monadic lazy list of nodes visited in order.

This is potentially very expensive. If you want to do efficient enumerations from a generation function, avoiding duplication up to equality or isomorphism, use Brendan McKay's method of "generation by canonical construction path".

Equations
• One or more equations did not get rendered due to their size.
Instances For
def depthFirstRemovingDuplicates' {α : Type u_1} [BEq α] [] (f : αList α) (a : α) (maxDepth : optParam () none) :
List α

Variant of depthFirst, using an internal HashSet to record and avoid already visited nodes.

This version describes the graph using α → List α, and returns the list of nodes visited in order.

Equations
Instances For