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 |
(* | A strongly connected component, described by its head node and the remaining sub-components topologically ordered | *) |
| |
Node of |
(* | A single node without self loop | *) |
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 head : 'n partition -> 'n option
Return the first node of a partition or None if the partition is empty
val flatten : 'n partition -> 'n list
Transform the partition into a 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 :Stdlib.Format.formatter -> t -> unit
end
) ->
sig
..end
This functor provides the partitioning algorithm constructing a WTO.