structure StrataDDM.OutGraph (nodeCount : Nat) : Type

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

• StrataDDM.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) " }"

@[reducible, inline]

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

Equations

• StrataDDM.OutGraph.Node n = Fin n

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

Equations

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

def StrataDDM.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 StrataDDM.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 StrataDDM.OutGraph.ofEdges! (n : Nat) (edges : List (Nat × Nat)) : OutGraph n

Equations

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

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

Equations

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

def StrataDDM.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.