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.

structure Lean.SCC.Data : Type

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

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

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

@[reducible, inline]

abbrev Lean.SCC.M (α : Type) [BEq α] [Hashable α] : Type → Type

Equations

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

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.