Very simple implementation of Tarjan's SCC algorithm. Performance is not a goal here since we use this module to compiler mutually recursive definitions, where each function (and nested let-rec) in the mutual block is a vertex. So, the graphs are small.

source
structure Lean.SCC.Data :
Type

- index? : Option Nat
- lowlink? : Option Nat
- onStack : Bool

Instances For

source
structure Lean.SCC.State (α : Type) [BEq α] [Hashable α] :
Type

- stack : List α
- nextIndex : Nat
- data : Std.HashMap α Data
- sccs : List (List α)

Instances For

source
@[reducible, inline]
abbrev Lean.SCC.M (α : Type) [BEq α] [Hashable α] :
Type → Type
Equations

- Lean.SCC.M α = StateM (Lean.SCC.State α)

Instances For

source
def Lean.SCC.scc {α : Type} [BEq α] [Hashable α] (vertices : List α) (successorsOf : α → List α) :
List (List α)
Equations

- One or more equations did not get rendered due to their size.

Instances For