structure Strata.OutGraph (nodeCount : Nat) : Type

• edges : Vector (Array (Fin nodeCount)) nodeCount

def Strata.instInhabitedOutGraph.default {a✝ : Nat} : OutGraph a✝

Equations

• Strata.instInhabitedOutGraph.default = { edges := default }

instance Strata.instInhabitedOutGraph {a✝ : Nat} : Inhabited (OutGraph a✝)

Equations

• Strata.instInhabitedOutGraph = { default := Strata.instInhabitedOutGraph.default }

def Strata.instReprOutGraph.repr {nodeCount✝ : Nat} : OutGraph nodeCount✝ → Nat → Std.Format

Equations

• Strata.instReprOutGraph.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "edges" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.edges)).group) " }"

instance Strata.instReprOutGraph {nodeCount✝ : Nat} : Repr (OutGraph nodeCount✝)

Equations

• Strata.instReprOutGraph = { reprPrec := Strata.instReprOutGraph.repr }

@[reducible, inline]

abbrev Strata.OutGraph.Node (n : Nat) : Type

Equations

• Strata.OutGraph.Node n = Fin n

def Strata.OutGraph.empty (n : Nat) : OutGraph n

Equations

• Strata.OutGraph.empty n = { edges := Vector.replicate n ∅ }

def Strata.OutGraph.addEdge {n : Nat} (g : OutGraph n) (f t : Node n) : OutGraph n

Equations

• g.addEdge f t = { edges := Vector.modify✝ g.edges ⟨↑t, ⋯⟩ fun (x : Array (Fin n)) => x.push ⟨↑f, ⋯⟩ }

def Strata.OutGraph.addEdge! {n : Nat} (g : OutGraph n) (f t : Nat) : OutGraph n

Equations

• g.addEdge! f t = if fp : f ≥ n then panic (toString "Invalid from edge " ++ toString f) else if tp : t ≥ n then panic (toString "Invalid to edge " ++ toString t) else g.addEdge ⟨f, ⋯⟩ ⟨t, ⋯⟩

def Strata.OutGraph.ofEdges! (n : Nat) (edges : List (Nat × Nat)) : OutGraph n

Equations

• Strata.OutGraph.ofEdges! n edges = List.foldl (fun (g : Strata.OutGraph n) (x : Nat × Nat) => match x with | (f, t) => g.addEdge! f t) (Strata.OutGraph.empty n) edges

def Strata.OutGraph.nodesOut {n : Nat} (g : OutGraph n) (node : Node n) : Array (Node n)

Equations

• g.nodesOut node = g.edges[node]

def Strata.OutGraph.tarjan {n : Nat} (g : OutGraph n) : Array (Array (Node n))

This run Tarjan's algorithm to compute strongly connected components.

Results are ordered so that nodes in the group are in the same element if they are in the same strongly connected component and a node only appears in an array after all the nodes that have paths to it.

Equations

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