package grenier
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=e5362e6ad0e888526517415e78b9e8243bb0cc1b0c952201884148832ac4442f
sha512=4e2f16b52b3c2786a1b8e93156184fd69d448cea571ca839b6cb88ab73f380994d1561fe24c1523c43ed8fc42d2ac01b673a13b6151fff4af4f009923d3aaf37
doc/grenier.fastdom/Fastdom/index.html
Module Fastdom
A library to compute graph dominators using "A Simple, Fast Dominance Algorithm" by Keith D. Cooper, Timothy J. Harvey, Ken Kennedy.
Graph representation
type 'a graph = {memoize : 'b. ('a -> 'b) -> 'a -> 'b;(*
*)memoize fmemoizes a functionfover nodes of the graph. The function returned must evaluatef xat most once for each nodex. Iffraises an exception, the same exception must be propagated to the caller but it is not necessary to memoize it.successors : 'b. ('b -> 'a -> 'b) -> 'b -> 'a -> 'b;(*
*)successors f acc nfold over the successors of noden, threading and updating theaccvalue.
}Abstraction of graphs with nodes of type 'a. Instance of graph must be provided by the user of the library.
Dominance information
val node : 'a t -> 'aThe node to which this information applies.
dominator (node n) returns the information associated to the dominator of n. If n is its own dominator, then dominator (node n) == node n.
val is_reachable : 'a t -> boolis_reachable (node n) returns true iff n is reachable from entrypoint following the successors relation.
val postorder_index : 'a t -> intpostorder_index (node n) is the index of n in the postorder traversal of the graph (see dominance), starting from 0.
If n was not reachable from the entrypoint, post_order_index (node n) = -1
Though in this case, it is better to use is_reachable before to check the validity of the node.
Reverse the successors relation (on the subset of the graph reachable from entrypoint).
Dominance computation
dominance graph entrypoint = (info, map) computes the dominators of graph starting from entrypoint.
The info array is indexed by the postorder index of a vertex, see postorder_index.
map n is the dominance information of node n. If n is not reachable from entrypoint, then is_reachable (map n) = false.