Documentation

Mathlib.Data.MLList.DepthFirst

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.

@[deprecated]
partial def depthFirst' {α : Type u} {m : Type u → Type u} [Monad m] [Alternative m] (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.

@[deprecated]
def depthFirst {α : Type u} {m : Type u → Type u} [Monad m] [Alternative m] (f : αm α) (a : α) (maxDepth : optParam (Option Nat) 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
    @[deprecated]
    def depthFirstRemovingDuplicates {m : Type u → Type u} [Monad m] {α : Type u} [BEq α] [Hashable α] (f : αMLList m α) (a : α) (maxDepth : optParam (Option Nat) 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
      @[deprecated]
      def depthFirstRemovingDuplicates' {α : Type u} [BEq α] [Hashable α] (f : αList α) (a : α) (maxDepth : optParam (Option Nat) 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