Graph.WeakTopologicalWeak topological ordering of the vertices of a graph, as described by François Bourdoncle.
Weak topological ordering is an extension of topological ordering for potentially cyclic graphs.
A hierarchical ordering of a set is a well-parenthesized permutation of its elements with no consecutive (. The elements between two parentheses are called a component, and the first elements of a component is called the head. A weak topological ordering of a graph is a hierarchical ordering of its vertices such that for every edge u -> v of the graph, either u comes (strictly) before v, or v is the head of a component containing u.
One may notice that :
v1, ..., vN, the following trivial weak topological ordering is valid : (v1 (v2
(... (vN))...)).Weak topological ordering are useful for fixpoint computation (see ChaoticIteration). This module aims at computing weak topological orderings which improve the precision and the convergence speed of these analyses.
module type G = sig ... endMinimal graph signature for the algorithm
The type of the elements of a weak topological ordering over a set of 'a.
Vertex v represents a single vertex.Component (head, cs) is a component of the wto, that is a sequence of elements between two parentheses. head is the head of the component, that is the first element, which is guaranteed to be a vertex by definition. cs is the rest of the component.The type of a sequence of outermost elements in a weak topological ordering. This is also the type of a weak topological ordering over a set of 'a.
Folding over the elements of a weak topological ordering. They are given to the accumulating function according to their order.
Note that as elements present in an ordering of type t can contain values of type t itself due to the Component variant, this function should be used by defining a recursive function f, which will call fold_left with f used to define the first parameter.