Module Wto
module Wto: sig
.. end
Weak topological orderings (WTOs) are a hierarchical decomposition of the
a graph where each layer is topologically ordered and strongly connected
components are aggregated and ordered recursively. This is a very
convenient representation to describe an evaluation order to reach a
fixpoint.
type 'n
component =
| |
Component of 'n * 'n partition |
| |
Node of 'n |
Each component of the graph is either an individual node of the graph
(without) self loop, or a strongly connected component where a node is
designed as the head of the component and the remaining nodes are given
by a list of components topologically ordered.
type 'n
partition = 'n component list
A list of strongly connected components, sorted topologically
val flatten : 'n partition -> 'n list
val fold_heads : ('a -> 'n -> 'a) -> 'a -> 'n partition -> 'a
module Make: functor (
Node
:
sig
type
t
val equal : t -> t -> bool
val hash : t -> int
val pretty : Format.formatter -> t -> unit
end
) ->
sig
.. end
This functor provides the partitioning algorithm constructing a WTO.