# 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.

## Deprecation #

This material has been moved out of Mathlib to https://github.com/semorrison/lean-monadic-list.

A generalisation of `depthFirst`

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

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

- depthFirst f a (some d) = depthFirst' (fun (n : Nat) (a : α) => if n ≤ d then f a else failure) 0 a
- depthFirst f a = depthFirst' (fun (x : Nat) (a : α) => f a) 0 a

## Instances For

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

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

- depthFirstRemovingDuplicates' f a maxDepth = (depthFirstRemovingDuplicates (fun (a : α) => MLList.ofList (f a)) a maxDepth).force.get!